Theorem dfdm4 5471

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

Assertion

Ref	Expression
dfdm4	⊢ dom 𝐴 = ran ◡𝐴

Proof of Theorem dfdm4

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

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

Syntax hints:   = wceq 1632  ∃wex 1853  {cab 2746   class class class wbr 4804  ^◡ccnv 5265  dom cdm 5266  ran crn 5267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-cnv 5274  df-dm 5276  df-rn 5277

This theorem is referenced by:  dmcnvcnv  5503  rncnvcnv  5504  rncoeq  5544  cnvimass  5643  cnvimarndm  5644  dminxp  5732  cnvsn0  5761  rnsnopg  5773  dmmpt  5791  dmco  5804  cores2  5809  cnvssrndm  5818  unidmrn  5826  dfdm2  5828  funimacnv  6131  foimacnv  6315  funcocnv2  6322  fimacnv  6510  f1opw2  7053  cnvexg  7277  tz7.48-3  7708  fopwdom  8233  sbthlem4  8238  fodomr  8276  f1opwfi  8435  zorn2lem4  9513  trclublem  13935  relexpcnv  13974  unbenlem  15814  gsumpropd2lem  17474  pjdm  20253  paste  21300  hmeores  21776  icchmeo  22941  fcnvgreu  29781  ffsrn  29813  gsummpt2co  30089  coinfliprv  30853  itg2addnclem2  33775  rncnv  34394  lnmlmic  38160  dmnonrel  38398  cnvrcl0  38434  conrel1d  38457