Metamath Proof Explorer

Theorem inopab

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

Ref Expression
Assertion inopab ⊢ x y | φ ∩ x y | ψ = x y | φ ∧ ψ

Proof

Step Hyp Ref Expression
1 relopabv ⊢ Rel ⁡ x y | φ
2 relin1 ⊢ Rel ⁡ x y | φ → Rel ⁡ x y | φ ∩ x y | ψ
3 1 2 ax-mp ⊢ Rel ⁡ x y | φ ∩ x y | ψ
4 relopabv ⊢ Rel ⁡ x y | φ ∧ ψ
5 sban ⊢ z x w y φ ∧ w y ψ ↔ z x w y φ ∧ z x w y ψ
6 sban ⊢ w y φ ∧ ψ ↔ w y φ ∧ w y ψ
7 6 sbbii ⊢ z x w y φ ∧ ψ ↔ z x w y φ ∧ w y ψ
8 vopelopabsb ⊢ z w ∈ x y | φ ↔ z x w y φ
9 vopelopabsb ⊢ z w ∈ x y | ψ ↔ z x w y ψ
10 8 9 anbi12i ⊢ z w ∈ x y | φ ∧ z w ∈ x y | ψ ↔ z x w y φ ∧ z x w y ψ
11 5 7 10 3bitr4ri ⊢ z w ∈ x y | φ ∧ z w ∈ x y | ψ ↔ z x w y φ ∧ ψ
12 elin ⊢ z w ∈ x y | φ ∩ x y | ψ ↔ z w ∈ x y | φ ∧ z w ∈ x y | ψ
13 vopelopabsb ⊢ z w ∈ x y | φ ∧ ψ ↔ z x w y φ ∧ ψ
14 11 12 13 3bitr4i ⊢ z w ∈ x y | φ ∩ x y | ψ ↔ z w ∈ x y | φ ∧ ψ
15 3 4 14 eqrelriiv ⊢ x y | φ ∩ x y | ψ = x y | φ ∧ ψ