This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvoprab1

Description: Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008) (Revised by Mario Carneiro, 5-Dec-2016)

Ref Expression
Hypotheses cbvoprab1.1 ⊢ Ⅎ 𝑤 𝜑
cbvoprab1.2 ⊢ Ⅎ 𝑥 𝜓
cbvoprab1.3 ⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜓 ) )
Assertion cbvoprab1 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑤 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 }

Proof

Step Hyp Ref Expression
1 cbvoprab1.1 ⊢ Ⅎ 𝑤 𝜑
2 cbvoprab1.2 ⊢ Ⅎ 𝑥 𝜓
3 cbvoprab1.3 ⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜓 ) )
4 nfv ⊢ Ⅎ 𝑤 𝑣 = ⟨ 𝑥 , 𝑦 ⟩
5 4 1 nfan ⊢ Ⅎ 𝑤 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
6 5 nfex ⊢ Ⅎ 𝑤 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
7 nfv ⊢ Ⅎ 𝑥 𝑣 = ⟨ 𝑤 , 𝑦 ⟩
8 7 2 nfan ⊢ Ⅎ 𝑥 ( 𝑣 = ⟨ 𝑤 , 𝑦 ⟩ ∧ 𝜓 )
9 8 nfex ⊢ Ⅎ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑤 , 𝑦 ⟩ ∧ 𝜓 )
10 opeq1 ⊢ ( 𝑥 = 𝑤 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑤 , 𝑦 ⟩ )
11 10 eqeq2d ⊢ ( 𝑥 = 𝑤 → ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑣 = ⟨ 𝑤 , 𝑦 ⟩ ) )
12 11 3 anbi12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( 𝑣 = ⟨ 𝑤 , 𝑦 ⟩ ∧ 𝜓 ) ) )
13 12 exbidv ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑣 = ⟨ 𝑤 , 𝑦 ⟩ ∧ 𝜓 ) ) )
14 6 9 13 cbvexv1 ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑣 = ⟨ 𝑤 , 𝑦 ⟩ ∧ 𝜓 ) )
15 14 opabbii ⊢ { ⟨ 𝑣 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } = { ⟨ 𝑣 , 𝑧 ⟩ ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑣 = ⟨ 𝑤 , 𝑦 ⟩ ∧ 𝜓 ) }
16 dfoprab2 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑣 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
17 dfoprab2 ⊢ { ⟨ ⟨ 𝑤 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } = { ⟨ 𝑣 , 𝑧 ⟩ ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑣 = ⟨ 𝑤 , 𝑦 ⟩ ∧ 𝜓 ) }
18 15 16 17 3eqtr4i ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑤 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 }