Theorem eqvinop

Description: A variable introduction law for ordered pairs. Analogue of Lemma 15 of Monk2 p. 109. (Contributed by NM, 28-May-1995)

	Ref	Expression
Hypotheses	eqvinop.1	⊢ 𝐵 ∈ V
	eqvinop.2	⊢ 𝐶 ∈ V
Assertion	eqvinop	⊢ ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		eqvinop.1	⊢ 𝐵 ∈ V
2		eqvinop.2	⊢ 𝐶 ∈ V
3	1 2	opth2	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) )
4	3	anbi2i	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ) )
5		ancom	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ) ↔ ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) )
6		anass	⊢ ( ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
7	4 5 6	3bitri	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
8	7	exbii	⊢ ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ∃ 𝑦 ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
9		19.42v	⊢ ( ∃ 𝑦 ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( 𝑥 = 𝐵 ∧ ∃ 𝑦 ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
10		opeq2	⊢ ( 𝑦 = 𝐶 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝐶 ⟩ )
11	10	eqeq2d	⊢ ( 𝑦 = 𝐶 → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ) )
12	2 11	ceqsexv	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ )
13	12	anbi2i	⊢ ( ( 𝑥 = 𝐵 ∧ ∃ 𝑦 ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ) )
14	8 9 13	3bitri	⊢ ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ) )
15	14	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ) )
16		opeq1	⊢ ( 𝑥 = 𝐵 → ⟨ 𝑥 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )
17	16	eqeq2d	⊢ ( 𝑥 = 𝐵 → ( 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ↔ 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ) )
18	1 17	ceqsexv	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 ⟩ ) ↔ 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ )
19	15 18	bitr2i	⊢ ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) )