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

Metamath Proof Explorer

Theorem dfrn2

Description: Alternate definition of range. Definition 4 of Suppes p. 60. (Contributed by NM, 27-Dec-1996)

Ref Expression
Assertion dfrn2 ⊢ ran ⁡ A = y | ∃ x x A y

Proof

Step Hyp Ref Expression
1 df-rn ⊢ ran ⁡ A = dom ⁡ A -1
2 df-dm ⊢ dom ⁡ A -1 = y | ∃ x y A -1 x
3 vex ⊢ y ∈ V
4 vex ⊢ x ∈ V
5 3 4 brcnv ⊢ y A -1 x ↔ x A y
6 5 exbii ⊢ ∃ x y A -1 x ↔ ∃ x x A y
7 6 abbii ⊢ y | ∃ x y A -1 x = y | ∃ x x A y
8 1 2 7 3eqtri ⊢ ran ⁡ A = y | ∃ x x A y