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 | ⊢ ( 𝐴 ∈ ( 𝐵 “ 𝐶 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐵 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elima.1 | ⊢ 𝐴 ∈ V | |
2 | 1 | elima | ⊢ ( 𝐴 ∈ ( 𝐵 “ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐶 𝑥 𝐵 𝐴 ) |
3 | df-rex | ⊢ ( ∃ 𝑥 ∈ 𝐶 𝑥 𝐵 𝐴 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐵 𝐴 ) ) | |
4 | 2 3 | bitri | ⊢ ( 𝐴 ∈ ( 𝐵 “ 𝐶 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐵 𝐴 ) ) |