Theorem isarep1

Description: Part of a study of the Axiom of Replacement used by the Isabelle prover. The object PrimReplace is apparently the image of the function encoded by ph ( x , y ) i.e. the class ( { <. x , y >. | ph } " A ) . If so, we can prove Isabelle's "Axiom of Replacement" conclusion without using the Axiom of Replacement, for which I (N. Megill) currently have no explanation. (Contributed by NM, 26-Oct-2006) (Proof shortened by Mario Carneiro, 4-Dec-2016)

	Ref	Expression
Assertion	isarep1	|- ( 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 )