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

Metamath Proof Explorer

Theorem dfdm4

Description: Alternate definition of domain. (Contributed by NM, 28-Dec-1996)

Ref Expression
Assertion dfdm4 ⊢ dom ⁡ A = ran ⁡ A -1

Proof

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