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

Metamath Proof Explorer

Theorem or2expropbilem2

Description: Lemma 2 for or2expropbi and ich2exprop . (Contributed by AV, 16-Jul-2023)

Ref Expression
Assertion or2expropbilem2 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 )
2 nfv ⊢ Ⅎ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 )
3 nfv ⊢ Ⅎ 𝑎 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
4 nfcv ⊢ Ⅎ 𝑎 𝑦
5 nfsbc1v ⊢ Ⅎ 𝑎 [ 𝑥 / 𝑎 ] 𝜑
6 4 5 nfsbcw ⊢ Ⅎ 𝑎 [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑
7 3 6 nfan ⊢ Ⅎ 𝑎 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
8 nfv ⊢ Ⅎ 𝑏 ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
9 nfsbc1v ⊢ Ⅎ 𝑏 [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑
10 8 9 nfan ⊢ Ⅎ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 )
11 opeq12 ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
12 11 eqeq2d ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
13 sbceq1a ⊢ ( 𝑎 = 𝑥 → ( 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜑 ) )
14 sbceq1a ⊢ ( 𝑏 = 𝑦 → ( [ 𝑥 / 𝑎 ] 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )
15 13 14 sylan9bb ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( 𝜑 ↔ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )
16 12 15 anbi12d ⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) ) )
17 1 2 7 10 16 cbvex2v ⊢ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )