Theorem rabxp

Description: Class abstraction restricted to a Cartesian product as an ordered-pair class abstraction. (Contributed by NM, 20-Feb-2014)

	Ref	Expression
Hypothesis	rabxp.1	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion	rabxp	⊢ { 𝑥 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) }

Proof

Step	Hyp	Ref	Expression
1		rabxp.1	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2		elxp	⊢ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
3	2	anbi1i	⊢ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) ↔ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝜑 ) )
4		19.41vv	⊢ ( ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝜑 ) ↔ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝜑 ) )
5		anass	⊢ ( ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝜑 ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝜑 ) ) )
6	1	anbi2d	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝜓 ) ) )
7		df-3an	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝜓 ) )
8	6 7	bitr4di	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) ) )
9	8	pm5.32i	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝜑 ) ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) ) )
10	5 9	bitri	⊢ ( ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝜑 ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) ) )
11	10	2exbii	⊢ ( ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) ) )
12	3 4 11	3bitr2i	⊢ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) ) )
13	12	abbii	⊢ { 𝑥 ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) } = { 𝑥 ∣ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) ) }
14		df-rab	⊢ { 𝑥 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) }
15		df-opab	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) } = { 𝑥 ∣ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) ) }
16	13 14 15	3eqtr4i	⊢ { 𝑥 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) }