Metamath Proof Explorer

Theorem elima3

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

Ref Expression
Hypothesis elima.1 ⊢ A ∈ V
Assertion elima3 ⊢ A ∈ B C ↔ ∃ x x ∈ C ∧ x A ∈ B

Proof

Step Hyp Ref Expression
1 elima.1 ⊢ A ∈ V
2 1 elima2 ⊢ A ∈ B C ↔ ∃ x x ∈ C ∧ x B A
3 df-br ⊢ x B A ↔ x A ∈ B
4 3 anbi2i ⊢ x ∈ C ∧ x B A ↔ x ∈ C ∧ x A ∈ B
5 4 exbii ⊢ ∃ x x ∈ C ∧ x B A ↔ ∃ x x ∈ C ∧ x A ∈ B
6 2 5 bitri ⊢ A ∈ B C ↔ ∃ x x ∈ C ∧ x A ∈ B