Metamath Proof Explorer


Theorem cbvopab1g

Description: Change first bound variable in an ordered-pair class abstraction, using explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See cbvopab1 for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 6-Oct-2004) (Revised by Mario Carneiro, 14-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses cbvopab1g.1 z φ
cbvopab1g.2 x ψ
cbvopab1g.3 x = z φ ψ
Assertion cbvopab1g x y | φ = z y | ψ

Proof

Step Hyp Ref Expression
1 cbvopab1g.1 z φ
2 cbvopab1g.2 x ψ
3 cbvopab1g.3 x = z φ ψ
4 nfv v y w = x y φ
5 nfv x w = v y
6 nfs1v x v x φ
7 5 6 nfan x w = v y v x φ
8 7 nfex x y w = v y v x φ
9 opeq1 x = v x y = v y
10 9 eqeq2d x = v w = x y w = v y
11 sbequ12 x = v φ v x φ
12 10 11 anbi12d x = v w = x y φ w = v y v x φ
13 12 exbidv x = v y w = x y φ y w = v y v x φ
14 4 8 13 cbvexv1 x y w = x y φ v y w = v y v x φ
15 nfv z w = v y
16 1 nfsb z v x φ
17 15 16 nfan z w = v y v x φ
18 17 nfex z y w = v y v x φ
19 nfv v y w = z y ψ
20 opeq1 v = z v y = z y
21 20 eqeq2d v = z w = v y w = z y
22 sbequ v = z v x φ z x φ
23 2 3 sbie z x φ ψ
24 22 23 bitrdi v = z v x φ ψ
25 21 24 anbi12d v = z w = v y v x φ w = z y ψ
26 25 exbidv v = z y w = v y v x φ y w = z y ψ
27 18 19 26 cbvexv1 v y w = v y v x φ z y w = z y ψ
28 14 27 bitri x y w = x y φ z y w = z y ψ
29 28 abbii w | x y w = x y φ = w | z y w = z y ψ
30 df-opab x y | φ = w | x y w = x y φ
31 df-opab z y | ψ = w | z y w = z y ψ
32 29 30 31 3eqtr4i x y | φ = z y | ψ