Metamath Proof Explorer


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 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 opelopabsb z b x y | φ [˙z / x]˙ [˙b / y]˙ φ
5 sbsbc b y φ [˙b / y]˙ φ
6 5 sbbii z x b y φ z x [˙b / y]˙ φ
7 sbsbc z x [˙b / y]˙ φ [˙z / x]˙ [˙b / y]˙ φ
8 6 7 bitr2i [˙z / x]˙ [˙b / y]˙ φ z x b y φ
9 3 4 8 3bitri z x y | φ b z x b y φ
10 9 rexbii z A z x y | φ b z A z x b y φ
11 nfs1v x z x b y φ
12 nfv z b y φ
13 sbequ12r z = x z x b y φ b y φ
14 11 12 13 cbvrexw z A z x b y φ x A b y φ
15 2 10 14 3bitri b x y | φ A x A b y φ