Metamath Proof Explorer


Theorem bnj1143

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj1143 xABB

Proof

Step Hyp Ref Expression
1 df-iun xAB=y|xAyB
2 notnotb A=¬¬A=
3 neq0 ¬A=xxA
4 2 3 xchbinx A=¬xxA
5 df-rex xAzBxxAzB
6 exsimpl xxAzBxxA
7 5 6 sylbi xAzBxxA
8 7 con3i ¬xxA¬xAzB
9 4 8 sylbi A=¬xAzB
10 9 alrimiv A=z¬xAzB
11 notnotb y|xAyB=¬¬y|xAyB=
12 neq0 ¬xAB=zzxAB
13 1 eqeq1i xAB=y|xAyB=
14 13 notbii ¬xAB=¬y|xAyB=
15 df-iun xAB=z|xAzB
16 15 eleq2i zxABzz|xAzB
17 16 exbii zzxABzzz|xAzB
18 12 14 17 3bitr3i ¬y|xAyB=zzz|xAzB
19 11 18 xchbinx y|xAyB=¬zzz|xAzB
20 alnex z¬zz|xAzB¬zzz|xAzB
21 abid zz|xAzBxAzB
22 21 notbii ¬zz|xAzB¬xAzB
23 22 albii z¬zz|xAzBz¬xAzB
24 19 20 23 3bitr2i y|xAyB=z¬xAzB
25 10 24 sylibr A=y|xAyB=
26 1 25 eqtrid A=xAB=
27 0ss B
28 26 27 eqsstrdi A=xABB
29 iunconst AxAB=B
30 eqimss xAB=BxABB
31 29 30 syl AxABB
32 28 31 pm2.61ine xABB