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	⊢ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑦 / 𝑏 ] [ 𝑥 / 𝑎 ] 𝜑 ) )