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

Metamath Proof Explorer

Theorem bnj1405

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

Ref Expression
Hypothesis bnj1405.1 ⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 )
Assertion bnj1405 ( 𝜑 → ∃ 𝑦 ∈ 𝐴 𝑋 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 bnj1405.1 ⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 )
2 eliun ⊢ ( 𝑋 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃ 𝑦 ∈ 𝐴 𝑋 ∈ 𝐵 )
3 1 2 sylib ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐴 𝑋 ∈ 𝐵 )