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

Metamath Proof Explorer

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 ⊢ { 𝑥 ∈ ( 𝐴 × 𝐵 ) ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ∧ 𝜓 ) }