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 relopab ⊢ Rel ⁡ x y | φ
2 relin1 ⊢ Rel ⁡ x y | φ → Rel ⁡ x y | φ ∩ x y | ψ
3 1 2 ax-mp ⊢ Rel ⁡ x y | φ ∩ x y | ψ
4 relopab ⊢ Rel ⁡ x y | φ ∧ ψ
5 sban ⊢ w y z x φ ∧ z x ψ ↔ w y z x φ ∧ w y z x ψ
6 sban ⊢ z x φ ∧ ψ ↔ z x φ ∧ z x ψ
7 6 sbbii ⊢ w y z x φ ∧ ψ ↔ w y z x φ ∧ z x ψ
8 opelopabsbALT ⊢ z w ∈ x y | φ ↔ w y z x φ
9 opelopabsbALT ⊢ z w ∈ x y | ψ ↔ w y z x ψ
10 8 9 anbi12i ⊢ z w ∈ x y | φ ∧ z w ∈ x y | ψ ↔ w y z x φ ∧ w y z x ψ
11 5 7 10 3bitr4ri ⊢ z w ∈ x y | φ ∧ z w ∈ x y | ψ ↔ w y z x φ ∧ ψ
12 elin ⊢ z w ∈ x y | φ ∩ x y | ψ ↔ z w ∈ x y | φ ∧ z w ∈ x y | ψ
13 opelopabsbALT ⊢ z w ∈ x y | φ ∧ ψ ↔ w y z x φ ∧ ψ
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 | φ ∧ ψ