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

Metamath Proof Explorer

Theorem inopab

Description: Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002)

Ref Expression
Assertion inopab ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) }

Proof

Step Hyp Ref Expression
1 relopabv ⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2 relin1 ⊢ ( Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → Rel ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) )
3 1 2 ax-mp ⊢ Rel ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
4 relopabv ⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) }
5 sban ⊢ ( [ 𝑧 / 𝑥 ] ( [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑤 / 𝑦 ] 𝜓 ) ↔ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 ) )
6 sban ⊢ ( [ 𝑤 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑤 / 𝑦 ] 𝜓 ) )
7 6 sbbii ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ [ 𝑧 / 𝑥 ] ( [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑤 / 𝑦 ] 𝜓 ) )
8 vopelopabsb ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
9 vopelopabsb ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 )
10 8 9 anbi12i ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 ) )
11 5 7 10 3bitr4ri ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) )
12 elin ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) )
13 vopelopabsb ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) )
14 11 12 13 3bitr4i ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } )
15 3 4 14 eqrelriiv ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) }