Theorem dfdm4

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

	Ref	Expression
Assertion	dfdm4	⊢ dom 𝐴 = ran ◡ 𝐴

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑦 ∈ V
2		vex	⊢ 𝑥 ∈ V
3	1 2	brcnv	⊢ ( 𝑦 ◡ 𝐴 𝑥 ↔ 𝑥 𝐴 𝑦 )
4	3	exbii	⊢ ( ∃ 𝑦 𝑦 ◡ 𝐴 𝑥 ↔ ∃ 𝑦 𝑥 𝐴 𝑦 )
5	4	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 𝑦 ◡ 𝐴 𝑥 } = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }
6		dfrn2	⊢ ran ◡ 𝐴 = { 𝑥 ∣ ∃ 𝑦 𝑦 ◡ 𝐴 𝑥 }
7		df-dm	⊢ dom 𝐴 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }
8	5 6 7	3eqtr4ri	⊢ dom 𝐴 = ran ◡ 𝐴