Metamath Proof Explorer

Theorem bnj1138

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

Ref Expression
Hypothesis bnj1138.1 
|- A = ( B u. C )
Assertion bnj1138 
|- ( X e. A <-> ( X e. B \/ X e. C ) )

Proof

Step Hyp Ref Expression
1 bnj1138.1 
 |-  A = ( B u. C )
2 1 eleq2i 
 |-  ( X e. A <-> X e. ( B u. C ) )
3 elun 
 |-  ( X e. ( B u. C ) <-> ( X e. B \/ X e. C ) )
4 2 3 bitri 
 |-  ( X e. A <-> ( X e. B \/ X e. C ) )