Metamath Proof Explorer


Theorem cbvopab

Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003)

Ref Expression
Hypotheses cbvopab.1 z φ
cbvopab.2 w φ
cbvopab.3 x ψ
cbvopab.4 y ψ
cbvopab.5 x = z y = w φ ψ
Assertion cbvopab x y | φ = z w | ψ

Proof

Step Hyp Ref Expression
1 cbvopab.1 z φ
2 cbvopab.2 w φ
3 cbvopab.3 x ψ
4 cbvopab.4 y ψ
5 cbvopab.5 x = z y = w φ ψ
6 nfv z v = x y
7 6 1 nfan z v = x y φ
8 nfv w v = x y
9 8 2 nfan w v = x y φ
10 nfv x v = z w
11 10 3 nfan x v = z w ψ
12 nfv y v = z w
13 12 4 nfan y v = z w ψ
14 opeq12 x = z y = w x y = z w
15 14 eqeq2d x = z y = w v = x y v = z w
16 15 5 anbi12d x = z y = w v = x y φ v = z w ψ
17 7 9 11 13 16 cbvex2v x y v = x y φ z w v = z w ψ
18 17 abbii v | x y v = x y φ = v | z w v = z w ψ
19 df-opab x y | φ = v | x y v = x y φ
20 df-opab z w | ψ = v | z w v = z w ψ
21 18 19 20 3eqtr4i x y | φ = z w | ψ