Theorem dfdm4 5804

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 3436	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3436	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5791	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1850	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2808	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5797	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5599	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2777	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1539  ∃wex 1782  {cab 2715   class class class wbr 5074  ^◡ccnv 5588  dom cdm 5589  ran crn 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-cnv 5597  df-dm 5599  df-rn 5600

This theorem is referenced by:  dmcnvcnv  5842  rncnvcnv  5843  rncoeq  5884  cnvimass  5989  cnvimarndm  5990  dminxp  6083  cnvsn0  6113  rnsnopg  6124  dmmpt  6143  dmco  6158  cores2  6163  cnvssrndm  6174  unidmrn  6182  dfdm2  6184  funimacnv  6515  foimacnv  6733  funcocnv2  6741  fimacnvOLD  6948  f1opw2  7524  cnvexg  7771  tz7.48-3  8275  fopwdom  8867  sbthlem4  8873  fodomr  8915  cnvfi  8963  f1opwfi  9123  zorn2lem4  10255  trclublem  14706  relexpcnv  14746  unbenlem  16609  gsumpropd2lem  18363  pjdm  20914  paste  22445  hmeores  22922  icchmeo  24104  fcnvgreu  31010  ffsrn  31064  gsummpt2co  31308  tocycfvres1  31377  tocycfvres2  31378  cycpmfvlem  31379  cycpmfv3  31382  coinfliprv  32449  itg2addnclem2  35829  rncnv  36436  lnmlmic  40913  dmnonrel  41198  cnvrcl0  41233  conrel1d  41271