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