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) (Proof shortened by SN, 19-Dec-2024)

	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		vopelopabsb	|- ( <. z , b >. e. { <. x , y >. | ph } <-> [ z / x ] [ b / y ] ph )
5	3 4	bitri	|- ( z { <. x , y >. | ph } b <-> [ z / x ] [ b / y ] ph )
6	5	rexbii	|- ( E. z e. A z { <. x , y >. | ph } b <-> E. z e. A [ z / x ] [ b / y ] ph )
7		nfs1v	|- F/ x [ z / x ] [ b / y ] ph
8		nfv	|- F/ z [ b / y ] ph
9		sbequ12r	|- ( z = x -> ( [ z / x ] [ b / y ] ph <-> [ b / y ] ph ) )
10	7 8 9	cbvrexw	|- ( E. z e. A [ z / x ] [ b / y ] ph <-> E. x e. A [ b / y ] ph )
11	2 6 10	3bitri	|- ( b e. ( { <. x , y >. | ph } " A ) <-> E. x e. A [ b / y ] ph )