This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )