You can use the Reexpress command to rewrite a
given or a goal in a different but equivalent way. Select the given or
goal that you want to reexpress and give the Reexpress command. A dialog
box will open, offering a number of different ways of reexpressing the
selected statement. (Double-clicking on a given or goal is a shortcut for
selecting it and giving the Reexpress command.) The statement to be
reexpressed appears at the top of the dialog box, and initially the entire
statement is selected. You can apply a reexpression to only part of the
statement by selecting the part you want to reexpress. Selecting works in
the usual way, except that when you drag the mouse across a part of the
statement, what gets selected is *the smallest meaningful subexpression
containing the symbols you drag across*. For example, if you drag the
mouse across the symbols “*x*∈” in the
statement “*x*∈*A*∧*y*∈*B*”,
what will be selected is the
statement “*x*∈*A*”.
Click on the buttons in the dialog box to perform the indicated
reexpressions on the selected part of the statement.

Once you have reexpressed the statement in the way you want, click the
OK button. The new version of the statement will be listed as a
*variant* of the original in the list of givens and goals. A
variant of a given or goal is listed below the original and indented. You
can select a variant and apply commands to it just like any other given or
goal.

Here is what the various buttons in the Reexpress dialog box do:

- Rename Bound Variable: This button can only be used when the selected
expression starts with a quantifier. Use this button to rename the
quantified variable. For example, you can rewrite
“∀
*x*(*x*∈*A*)” as “∀*y*(*y*∈*A*)”. - (...): Use this button to add parentheses around an expression. If the statement has brackets around it, they are changed to parentheses. You can't use this button if adding parentheses would change the meaning of the statement; it's only for making the statement easier to read. (There are a few cases in which parentheses affect the workings of a command. For more information, see the Cases, Conjoin, Conjunction, Disjunction, Disjunctive Syllogism, Addition, and Split Up commands.)
- [...]: Like (...).
- Remove ( ) or [ ]: Use this button to remove parentheses or brackets around an expression. Again, you can't do this if it would change the meaning of the statement.
- Reexpress Negative/Make Negative: When the selected expression starts
with “¬”, this button is called
Reexpress Negative. Use it to reexpress the negative statement as an
equivalent positive one. For example,
“¬∀
*x*(*x*∈*A*)” gets reexpressed as “∃*x*(*x*∉*A*)” and “¬(*x*∈*A*∧*x*∈*B*)” becomes “*x*∉*A*∨*x*∉*B*”. If the “¬” symbol is followed by several quantifiers, pushing this button repeatedly will move the “¬” past the quantifiers one at a time. When the selected expression does not start with “¬”, this button is called Make Negative, and it reexpresses the expression as an equivalent one starting with “¬”. Often this reverses the effect of the Reexpress Negative button. - Apply Definition: This button performs a number of different
reexpressions, based on the definitions of symbols appearing in the
selected expression. For example, “
*x*=*y*” gets reexpressed as “∀*a*(*a*∈*x*↔*a*∈*y*)”, “*x*⊆*y*” gets reexpressed as “∀*a*(*a*∈*x*→*a*∈*y*)”, and “*x*∈*A*∩*B*” gets reexpressed as “*x*∈*A*∧*x*∈*B*”. Here is a list of all the reexpressions performed by this button:Statements of this form: Are reexpressed like this: *A*⊆*B*∀ *a*(*a*∈*A*→*a*∈*B*)*A*=∅¬∃ *a*(*a*∈*A*)( *a*,*b*)=(*c*,*d*)*a*=*c*∧*b*=*d**A*=*B*∀ *a*(*a*∈*A*↔*a*∈*B*)*x*∈∅*x*≠*x**x*∈{*a*_{1},*a*_{2},…,*a*_{n}}*x*=*a*_{1}∨*x*=*a*_{2}∨…∨*x*=*a*_{n}*x*∈*A*_{1}∩*A*_{2}∩…∩*A*_{n}*x*∈*A*_{1}∧*x*∈*A*_{2}∧…∧*x*∈*A*_{n}*x*∈*A*_{1}∪*A*_{2}∪…∪*A*_{n}*x*∈*A*_{1}∨*x*∈*A*_{2}∨…∨*x*∈*A*_{n}*x*∈*A*△*B*( *x*∈*A*∖*B*)∨(*x*∈*B*∖*A*)*x*∈*A*∖*B**x*∈*A*∧*x*∉*B*( *a*,*b*)∈*A*×*B**a*∈*A*∧*b*∈*B**x*∈*A*×*B*∃ *a*∈*A*∃*b*∈*B*(*x*=(*a*,*b*))( *a*,*b*)∈*R*○*S*∃ *c*((*a*,*c*)∈*S*∧(*c*,*b*)∈*R*)*x*∈*R*○*S*∃ *a*∃*b*∃*c*((*a*,*b*)∈*S*∧(*b*,*c*)∈*R*∧*x*=(*a*,*c*))*x*∈*U*∩∩*F**x*∈*U*∧∀*A*∈*F*(*x*∈*A*)*x*∈∪*F*∃ *A*∈*F*(*x*∈*A*)*x*∈𝒫(*A*)*x*⊆*A*( *a*,*b*)∈*R*^{−1}( *b*,*a*)∈*R**x*∈*R*^{−1}∃ *a*∃*b*(*x*=(*a*,*b*)∧(*b*,*a*)∈*R*)*x*∈{*y*∈*A*|*P*(*y*)}*x*∈*A*∧*P*(*x*)*x*∈{*f*(*y*)|*y*∈*A*}∃ *y*∈*A*(*x*=*f*(*y*))*x*∈(*a*,*b*)*x*={*a*}∨*x*={*a*,*b*}∀ *x*∈*A**P*(*x*)∀ *x*(*x*∈*A*→*P*(*x*))∃ *x*∈*A**P*(*x*)∃ *x*(*x*∈*A*∧*P*(*x*))∃! *x**P*(*x*)∃ *x*(*P*(*x*)∧∀*y*(*P*(*y*)→*y*=*x*))