This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- U_ x e. A B C_ B

Proof

Step Hyp Ref Expression
1 df-iun 
 |-  U_ x e. A B = { y | E. x e. A y e. B }
2 notnotb 
 |-  ( A = (/) <-> -. -. A = (/) )
3 neq0 
 |-  ( -. A = (/) <-> E. x x e. A )
4 2 3 xchbinx 
 |-  ( A = (/) <-> -. E. x x e. A )
5 df-rex 
 |-  ( E. x e. A z e. B <-> E. x ( x e. A /\ z e. B ) )
6 exsimpl 
 |-  ( E. x ( x e. A /\ z e. B ) -> E. x x e. A )
7 5 6 sylbi 
 |-  ( E. x e. A z e. B -> E. x x e. A )
8 7 con3i 
 |-  ( -. E. x x e. A -> -. E. x e. A z e. B )
9 4 8 sylbi 
 |-  ( A = (/) -> -. E. x e. A z e. B )
10 9 alrimiv 
 |-  ( A = (/) -> A. z -. E. x e. A z e. B )
11 notnotb 
 |-  ( { y | E. x e. A y e. B } = (/) <-> -. -. { y | E. x e. A y e. B } = (/) )
12 neq0 
 |-  ( -. U_ x e. A B = (/) <-> E. z z e. U_ x e. A B )
13 1 eqeq1i 
 |-  ( U_ x e. A B = (/) <-> { y | E. x e. A y e. B } = (/) )
14 13 notbii 
 |-  ( -. U_ x e. A B = (/) <-> -. { y | E. x e. A y e. B } = (/) )
15 df-iun 
 |-  U_ x e. A B = { z | E. x e. A z e. B }
16 15 eleq2i 
 |-  ( z e. U_ x e. A B <-> z e. { z | E. x e. A z e. B } )
17 16 exbii 
 |-  ( E. z z e. U_ x e. A B <-> E. z z e. { z | E. x e. A z e. B } )
18 12 14 17 3bitr3i 
 |-  ( -. { y | E. x e. A y e. B } = (/) <-> E. z z e. { z | E. x e. A z e. B } )
19 11 18 xchbinx 
 |-  ( { y | E. x e. A y e. B } = (/) <-> -. E. z z e. { z | E. x e. A z e. B } )
20 alnex 
 |-  ( A. z -. z e. { z | E. x e. A z e. B } <-> -. E. z z e. { z | E. x e. A z e. B } )
21 abid 
 |-  ( z e. { z | E. x e. A z e. B } <-> E. x e. A z e. B )
22 21 notbii 
 |-  ( -. z e. { z | E. x e. A z e. B } <-> -. E. x e. A z e. B )
23 22 albii 
 |-  ( A. z -. z e. { z | E. x e. A z e. B } <-> A. z -. E. x e. A z e. B )
24 19 20 23 3bitr2i 
 |-  ( { y | E. x e. A y e. B } = (/) <-> A. z -. E. x e. A z e. B )
25 10 24 sylibr 
 |-  ( A = (/) -> { y | E. x e. A y e. B } = (/) )
26 1 25 eqtrid 
 |-  ( A = (/) -> U_ x e. A B = (/) )
27 0ss 
 |-  (/) C_ B
28 26 27 eqsstrdi 
 |-  ( A = (/) -> U_ x e. A B C_ B )
29 iunconst 
 |-  ( A =/= (/) -> U_ x e. A B = B )
30 eqimss 
 |-  ( U_ x e. A B = B -> U_ x e. A B C_ B )
31 29 30 syl 
 |-  ( A =/= (/) -> U_ x e. A B C_ B )
32 28 31 pm2.61ine 
 |-  U_ x e. A B C_ B