Metamath Proof Explorer

Theorem difopab

Description: Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015) (Proof shortened by SN, 19-Dec-2024)

Ref Expression
Assertion difopab ⊢ x y | φ ∖ x y | ψ = x y | φ ∧ ¬ ψ

Proof

Step Hyp Ref Expression
1 relopabv ⊢ Rel ⁡ x y | φ
2 reldif ⊢ 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 sbn ⊢ z x ¬ w y ψ ↔ ¬ z x w y ψ
10 sbn ⊢ w y ¬ ψ ↔ ¬ w y ψ
11 10 sbbii ⊢ z x w y ¬ ψ ↔ z x ¬ w y ψ
12 vopelopabsb ⊢ z w ∈ x y | ψ ↔ z x w y ψ
13 12 notbii ⊢ ¬ z w ∈ x y | ψ ↔ ¬ z x w y ψ
14 9 11 13 3bitr4ri ⊢ ¬ z w ∈ x y | ψ ↔ z x w y ¬ ψ
15 8 14 anbi12i ⊢ z w ∈ x y | φ ∧ ¬ z w ∈ x y | ψ ↔ z x w y φ ∧ z x w y ¬ ψ
16 5 7 15 3bitr4ri ⊢ z w ∈ x y | φ ∧ ¬ z w ∈ x y | ψ ↔ z x w y φ ∧ ¬ ψ
17 eldif ⊢ z w ∈ x y | φ ∖ x y | ψ ↔ z w ∈ x y | φ ∧ ¬ z w ∈ x y | ψ
18 vopelopabsb ⊢ z w ∈ x y | φ ∧ ¬ ψ ↔ z x w y φ ∧ ¬ ψ
19 16 17 18 3bitr4i ⊢ z w ∈ x y | φ ∖ x y | ψ ↔ z w ∈ x y | φ ∧ ¬ ψ
20 3 4 19 eqrelriiv ⊢ x y | φ ∖ x y | ψ = x y | φ ∧ ¬ ψ