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 ⊢ 𝐴 ∈ V
Assertion elima3 ( 𝐴 ∈ ( 𝐵 “ 𝐶 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elima.1 ⊢ 𝐴 ∈ V
2 1 elima2 ⊢ ( 𝐴 ∈ ( 𝐵 “ 𝐶 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐵 𝐴 ) )
3 df-br ⊢ ( 𝑥 𝐵 𝐴 ↔ ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝐵 )
4 3 anbi2i ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐵 𝐴 ) ↔ ( 𝑥 ∈ 𝐶 ∧ ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝐵 ) )
5 4 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐵 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝐵 ) )
6 2 5 bitri ⊢ ( 𝐴 ∈ ( 𝐵 “ 𝐶 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝐵 ) )