This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elrng

Description: Membership in a range. (Contributed by Scott Fenton, 2-Feb-2011)

Ref Expression
Assertion elrng ⊢ A ∈ V → A ∈ ran ⁡ B ↔ ∃ x x B A

Proof

Step Hyp Ref Expression
1 elrn2g ⊢ A ∈ V → A ∈ ran ⁡ B ↔ ∃ x x A ∈ B
2 df-br ⊢ x B A ↔ x A ∈ B
3 2 exbii ⊢ ∃ x x B A ↔ ∃ x x A ∈ B
4 1 3 bitr4di ⊢ A ∈ V → A ∈ ran ⁡ B ↔ ∃ x x B A