Metamath Proof Explorer

Theorem wopprc

Description: Unrelated: Wiener pairs treat proper classes symmetrically. (Contributed by Stefan O'Rear, 19-Sep-2014)

Ref Expression
Assertion wopprc ⊢ A ∈ V ∧ B ∈ V ↔ ¬ 1 𝑜 ∈ A ∅ B

Proof

Step Hyp Ref Expression
1 id ⊢ ∅ = A ∅ → ∅ = A ∅
2 dfsn2 ⊢ ∅ = ∅ ∅
3 1 2 eqtr3di ⊢ ∅ = A ∅ → A ∅ = ∅ ∅
4 snex ⊢ A ∈ V
5 0ex ⊢ ∅ ∈ V
6 4 5 preqr1 ⊢ A ∅ = ∅ ∅ → A = ∅
7 3 6 syl ⊢ ∅ = A ∅ → A = ∅
8 snprc ⊢ ¬ A ∈ V ↔ A = ∅
9 7 8 sylibr ⊢ ∅ = A ∅ → ¬ A ∈ V
10 8 biimpi ⊢ ¬ A ∈ V → A = ∅
11 10 preq1d ⊢ ¬ A ∈ V → A ∅ = ∅ ∅
12 2 11 eqtr4id ⊢ ¬ A ∈ V → ∅ = A ∅
13 9 12 impbii ⊢ ∅ = A ∅ ↔ ¬ A ∈ V
14 13 con2bii ⊢ A ∈ V ↔ ¬ ∅ = A ∅
15 snprc ⊢ ¬ B ∈ V ↔ B = ∅
16 eqcom ⊢ B = ∅ ↔ ∅ = B
17 15 16 bitr2i ⊢ ∅ = B ↔ ¬ B ∈ V
18 17 con2bii ⊢ B ∈ V ↔ ¬ ∅ = B
19 5 sneqr ⊢ ∅ = B → ∅ = B
20 sneq ⊢ ∅ = B → ∅ = B
21 19 20 impbii ⊢ ∅ = B ↔ ∅ = B
22 18 21 xchbinxr ⊢ B ∈ V ↔ ¬ ∅ = B
23 14 22 anbi12i ⊢ A ∈ V ∧ B ∈ V ↔ ¬ ∅ = A ∅ ∧ ¬ ∅ = B
24 pm4.56 ⊢ ¬ ∅ = A ∅ ∧ ¬ ∅ = B ↔ ¬ ∅ = A ∅ ∨ ∅ = B
25 snex ⊢ ∅ ∈ V
26 25 elpr ⊢ ∅ ∈ A ∅ B ↔ ∅ = A ∅ ∨ ∅ = B
27 24 26 xchbinxr ⊢ ¬ ∅ = A ∅ ∧ ¬ ∅ = B ↔ ¬ ∅ ∈ A ∅ B
28 23 27 bitri ⊢ A ∈ V ∧ B ∈ V ↔ ¬ ∅ ∈ A ∅ B
29 df1o2 ⊢ 1 𝑜 = ∅
30 29 eleq1i ⊢ 1 𝑜 ∈ A ∅ B ↔ ∅ ∈ A ∅ B
31 28 30 xchbinxr ⊢ A ∈ V ∧ B ∈ V ↔ ¬ 1 𝑜 ∈ A ∅ B