If you have a given of the form x=y, then in any given or goal you may substitute y for x or x for y. To perform such a substitution, select the given or goal in which you would like to do the substitution and give the Substitute command. A dialog box will open. The statement in which the substitution is to be performed appears at the top of the dialog box, and initially the entire statement is selected. You can perform the substitution in only part of the statement by selecting the part in which you want the substitution to be performed. 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 word “Substitute” in the dialog box, and a menu will appear showing all available substitutions; an entry of the form “x⇒y” means “replace x by y”. Select a substitution from the menu and the substitution will be performed. If no substitutions are available, there will be no Substitute menu in the dialog box. The other buttons in the dialog box can be used to rewrite the statement in some other ways; for details see the instructions for the Reexpress command.