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 𝐴 = ( 𝐵𝐶 )
Assertion bnj1138 ( 𝑋𝐴 ↔ ( 𝑋𝐵𝑋𝐶 ) )

Proof

Step Hyp Ref Expression
1 bnj1138.1 𝐴 = ( 𝐵𝐶 )
2 1 eleq2i ( 𝑋𝐴𝑋 ∈ ( 𝐵𝐶 ) )
3 elun ( 𝑋 ∈ ( 𝐵𝐶 ) ↔ ( 𝑋𝐵𝑋𝐶 ) )
4 2 3 bitri ( 𝑋𝐴 ↔ ( 𝑋𝐵𝑋𝐶 ) )