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 x y | φ A x A b y φ

Proof

Step Hyp Ref Expression
1 vex b V
2 1 elima b x y | φ A z A z x y | φ b
3 df-br z x y | φ b z b x y | φ
4 vopelopabsb z b x y | φ z x b y φ
5 3 4 bitri z x y | φ b z x b y φ
6 5 rexbii z A z x y | φ b z A z x b y φ
7 nfs1v x z x b y φ
8 nfv z b y φ
9 sbequ12r z = x z x b y φ b y φ
10 7 8 9 cbvrexw z A z x b y φ x A b y φ
11 2 6 10 3bitri b x y | φ A x A b y φ