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

Metamath Proof Explorer

Theorem bnj1146

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

Ref Expression
Hypothesis bnj1146.1 
|- ( y e. A -> A. x y e. A )
Assertion bnj1146 
|- U_ x e. A B C_ B

Proof

Step Hyp Ref Expression
1 bnj1146.1 
 |-  ( y e. A -> A. x y e. A )
2 nfv 
 |-  F/ y ( x e. A /\ w e. B )
3 1 nf5i 
 |-  F/ x y e. A
4 nfv 
 |-  F/ x w e. B
5 3 4 nfan 
 |-  F/ x ( y e. A /\ w e. B )
6 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
7 6 anbi1d 
 |-  ( x = y -> ( ( x e. A /\ w e. B ) <-> ( y e. A /\ w e. B ) ) )
8 2 5 7 cbvexv1 
 |-  ( E. x ( x e. A /\ w e. B ) <-> E. y ( y e. A /\ w e. B ) )
9 df-rex 
 |-  ( E. x e. A w e. B <-> E. x ( x e. A /\ w e. B ) )
10 df-rex 
 |-  ( E. y e. A w e. B <-> E. y ( y e. A /\ w e. B ) )
11 8 9 10 3bitr4i 
 |-  ( E. x e. A w e. B <-> E. y e. A w e. B )
12 11 abbii 
 |-  { w | E. x e. A w e. B } = { w | E. y e. A w e. B }
13 df-iun 
 |-  U_ x e. A B = { w | E. x e. A w e. B }
14 df-iun 
 |-  U_ y e. A B = { w | E. y e. A w e. B }
15 12 13 14 3eqtr4i 
 |-  U_ x e. A B = U_ y e. A B
16 bnj1143 
 |-  U_ y e. A B C_ B
17 15 16 eqsstri 
 |-  U_ x e. A B C_ B