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 ( 𝜑 → ∃ 𝑦𝐴 𝑋𝐵 )