Metamath Proof Explorer


Theorem elima2

Description: Membership in an image. Theorem 34 of Suppes p. 65. (Contributed by NM, 11-Aug-2004)

Ref Expression
Hypothesis elima.1 𝐴 ∈ V
Assertion elima2 ( 𝐴 ∈ ( 𝐵𝐶 ) ↔ ∃ 𝑥 ( 𝑥𝐶𝑥 𝐵 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elima.1 𝐴 ∈ V
2 1 elima ( 𝐴 ∈ ( 𝐵𝐶 ) ↔ ∃ 𝑥𝐶 𝑥 𝐵 𝐴 )
3 df-rex ( ∃ 𝑥𝐶 𝑥 𝐵 𝐴 ↔ ∃ 𝑥 ( 𝑥𝐶𝑥 𝐵 𝐴 ) )
4 2 3 bitri ( 𝐴 ∈ ( 𝐵𝐶 ) ↔ ∃ 𝑥 ( 𝑥𝐶𝑥 𝐵 𝐴 ) )