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 𝑧 𝜑
cbvopab1g.2 𝑥 𝜓
cbvopab1g.3 ( 𝑥 = 𝑧 → ( 𝜑𝜓 ) )
Assertion cbvopab1g { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝜓 }

Proof

Step Hyp Ref Expression
1 cbvopab1g.1 𝑧 𝜑
2 cbvopab1g.2 𝑥 𝜓
3 cbvopab1g.3 ( 𝑥 = 𝑧 → ( 𝜑𝜓 ) )
4 nfv 𝑣𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
5 nfv 𝑥 𝑤 = ⟨ 𝑣 , 𝑦
6 nfs1v 𝑥 [ 𝑣 / 𝑥 ] 𝜑
7 5 6 nfan 𝑥 ( 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ∧ [ 𝑣 / 𝑥 ] 𝜑 )
8 7 nfex 𝑥𝑦 ( 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ∧ [ 𝑣 / 𝑥 ] 𝜑 )
9 opeq1 ( 𝑥 = 𝑣 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑣 , 𝑦 ⟩ )
10 9 eqeq2d ( 𝑥 = 𝑣 → ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ) )
11 sbequ12 ( 𝑥 = 𝑣 → ( 𝜑 ↔ [ 𝑣 / 𝑥 ] 𝜑 ) )
12 10 11 anbi12d ( 𝑥 = 𝑣 → ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ∧ [ 𝑣 / 𝑥 ] 𝜑 ) ) )
13 12 exbidv ( 𝑥 = 𝑣 → ( ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ∧ [ 𝑣 / 𝑥 ] 𝜑 ) ) )
14 4 8 13 cbvexv1 ( ∃ 𝑥𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑣𝑦 ( 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ∧ [ 𝑣 / 𝑥 ] 𝜑 ) )
15 nfv 𝑧 𝑤 = ⟨ 𝑣 , 𝑦
16 1 nfsb 𝑧 [ 𝑣 / 𝑥 ] 𝜑
17 15 16 nfan 𝑧 ( 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ∧ [ 𝑣 / 𝑥 ] 𝜑 )
18 17 nfex 𝑧𝑦 ( 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ∧ [ 𝑣 / 𝑥 ] 𝜑 )
19 nfv 𝑣𝑦 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝜓 )
20 opeq1 ( 𝑣 = 𝑧 → ⟨ 𝑣 , 𝑦 ⟩ = ⟨ 𝑧 , 𝑦 ⟩ )
21 20 eqeq2d ( 𝑣 = 𝑧 → ( 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ↔ 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ) )
22 sbequ ( 𝑣 = 𝑧 → ( [ 𝑣 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
23 2 3 sbie ( [ 𝑧 / 𝑥 ] 𝜑𝜓 )
24 22 23 bitrdi ( 𝑣 = 𝑧 → ( [ 𝑣 / 𝑥 ] 𝜑𝜓 ) )
25 21 24 anbi12d ( 𝑣 = 𝑧 → ( ( 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ∧ [ 𝑣 / 𝑥 ] 𝜑 ) ↔ ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝜓 ) ) )
26 25 exbidv ( 𝑣 = 𝑧 → ( ∃ 𝑦 ( 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ∧ [ 𝑣 / 𝑥 ] 𝜑 ) ↔ ∃ 𝑦 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝜓 ) ) )
27 18 19 26 cbvexv1 ( ∃ 𝑣𝑦 ( 𝑤 = ⟨ 𝑣 , 𝑦 ⟩ ∧ [ 𝑣 / 𝑥 ] 𝜑 ) ↔ ∃ 𝑧𝑦 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝜓 ) )
28 14 27 bitri ( ∃ 𝑥𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧𝑦 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝜓 ) )
29 28 abbii { 𝑤 ∣ ∃ 𝑥𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } = { 𝑤 ∣ ∃ 𝑧𝑦 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝜓 ) }
30 df-opab { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
31 df-opab { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝜓 } = { 𝑤 ∣ ∃ 𝑧𝑦 ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝜓 ) }
32 29 30 31 3eqtr4i { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝜓 }