Theorem dfdm4 5834

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 3440	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3440	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5821	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1849	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2798	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5827	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5624	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2765	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1541  ∃wex 1780  {cab 2709   class class class wbr 5089  ^◡ccnv 5613  dom cdm 5614  ran crn 5615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-cnv 5622  df-dm 5624  df-rn 5625

This theorem is referenced by:  dmcnvcnv  5872  rncnvcnv  5873  rncoeq  5920  cnvimass  6030  cnvimarndm  6031  dminxp  6127  cnvsn0  6157  rnsnopg  6168  dmmpt  6187  dmco  6202  cores2  6207  cnvssrndm  6218  unidmrn  6226  dfdm2  6228  funimacnv  6562  foimacnv  6780  funcocnv2  6788  f1opw2  7601  cnvexg  7854  tz7.48-3  8363  fopwdom  8998  sbthlem4  9003  fodomr  9041  cnvfi  9085  fodomfir  9212  f1opwfi  9240  zorn2lem4  10390  trclublem  14902  relexpcnv  14942  unbenlem  16820  gsumpropd2lem  18587  pjdm  21644  paste  23209  hmeores  23686  icchmeo  24865  icchmeoOLD  24866  fcnvgreu  32655  ffsrn  32711  gsummpt2co  33028  tocycfvres1  33079  tocycfvres2  33080  cycpmfvlem  33081  cycpmfv3  33084  coinfliprv  34496  itg2addnclem2  37720  rncnv  38342  lnmlmic  43129  dmnonrel  43631  cnvrcl0  43666  conrel1d  43704