Theorem dfdm4 5852

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 3446	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3446	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5839	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1850	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2804	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5845	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5642	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2771	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1542  ∃wex 1781  {cab 2715   class class class wbr 5100  ^◡ccnv 5631  dom cdm 5632  ran crn 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  dmcnvcnv  5890  rncnvcnv  5891  rncoeq  5939  cnvimass  6049  cnvimarndm  6050  dminxp  6146  cnvsn0  6176  rnsnopg  6187  dmmpt  6206  dmco  6221  cores2  6226  cnvssrndm  6237  unidmrn  6245  dfdm2  6247  funimacnv  6581  foimacnv  6799  funcocnv2  6807  f1opw2  7623  cnvexg  7876  tz7.48-3  8385  fopwdom  9025  sbthlem4  9030  fodomr  9068  cnvfi  9112  fodomfir  9240  f1opwfi  9268  zorn2lem4  10421  trclublem  14930  relexpcnv  14970  unbenlem  16848  gsumpropd2lem  18616  pjdm  21674  paste  23250  hmeores  23727  icchmeo  24906  icchmeoOLD  24907  fcnvgreu  32762  ffsrn  32818  gsummpt2co  33142  tocycfvres1  33204  tocycfvres2  33205  cycpmfvlem  33206  cycpmfv3  33209  coinfliprv  34661  itg2addnclem2  37923  rncnv  38557  lnmlmic  43445  dmnonrel  43946  cnvrcl0  43981  conrel1d  44019