Theorem isarep1OLD

Description: Obsolete version of isarep1 as of 19-Dec-2024. (Contributed by NM, 26-Oct-2006) (Proof shortened by Mario Carneiro, 4-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	isarep1OLD	|- ( b e. ( { <. x , y >. | ph } " A ) <-> E. x e. A [ b / y ] ph )

Proof

Step	Hyp	Ref	Expression
1		vex	|- b e. _V
2	1	elima	|- ( b e. ( { <. x , y >. | ph } " A ) <-> E. z e. A z { <. x , y >. | ph } b )
3		df-br	|- ( z { <. x , y >. | ph } b <-> <. z , b >. e. { <. x , y >. | ph } )
4		opelopabsb	|- ( <. z , b >. e. { <. x , y >. | ph } <-> [. z / x ]. [. b / y ]. ph )
5		sbsbc	|- ( [ b / y ] ph <-> [. b / y ]. ph )
6	5	sbbii	|- ( [ z / x ] [ b / y ] ph <-> [ z / x ] [. b / y ]. ph )
7		sbsbc	|- ( [ z / x ] [. b / y ]. ph <-> [. z / x ]. [. b / y ]. ph )
8	6 7	bitr2i	|- ( [. z / x ]. [. b / y ]. ph <-> [ z / x ] [ b / y ] ph )
9	3 4 8	3bitri	|- ( z { <. x , y >. | ph } b <-> [ z / x ] [ b / y ] ph )
10	9	rexbii	|- ( E. z e. A z { <. x , y >. | ph } b <-> E. z e. A [ z / x ] [ b / y ] ph )
11		nfs1v	|- F/ x [ z / x ] [ b / y ] ph
12		nfv	|- F/ z [ b / y ] ph
13		sbequ12r	|- ( z = x -> ( [ z / x ] [ b / y ] ph <-> [ b / y ] ph ) )
14	11 12 13	cbvrexw	|- ( E. z e. A [ z / x ] [ b / y ] ph <-> E. x e. A [ b / y ] ph )
15	2 10 14	3bitri	|- ( b e. ( { <. x , y >. | ph } " A ) <-> E. x e. A [ b / y ] ph )