Metamath Proof Explorer

Theorem bnj226

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

Ref Expression
Hypothesis bnj226.1 
|- B C_ C
Assertion bnj226 
|- U_ x e. A B C_ C

Proof

Step Hyp Ref Expression
1 bnj226.1 
 |-  B C_ C
2 1 rgenw 
 |-  A. x e. A B C_ C
3 iunss 
 |-  ( U_ x e. A B C_ C <-> A. x e. A B C_ C )
4 2 3 mpbir 
 |-  U_ x e. A B C_ C