Theorem dfdm4 5896

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 3479	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3479	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5883	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1851	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2803	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5889	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5687	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2772	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1542  ∃wex 1782  {cab 2710   class class class wbr 5149  ^◡ccnv 5676  dom cdm 5677  ran crn 5678

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-cnv 5685  df-dm 5687  df-rn 5688

This theorem is referenced by:  dmcnvcnv  5933  rncnvcnv  5934  rncoeq  5975  cnvimass  6081  cnvimarndm  6082  dminxp  6180  cnvsn0  6210  rnsnopg  6221  dmmpt  6240  dmco  6254  cores2  6259  cnvssrndm  6271  unidmrn  6279  dfdm2  6281  funimacnv  6630  foimacnv  6851  funcocnv2  6859  fimacnvOLD  7073  f1opw2  7661  cnvexg  7915  tz7.48-3  8444  fopwdom  9080  sbthlem4  9086  fodomr  9128  cnvfi  9180  f1opwfi  9356  zorn2lem4  10494  trclublem  14942  relexpcnv  14982  unbenlem  16841  gsumpropd2lem  18598  pjdm  21262  paste  22798  hmeores  23275  icchmeo  24457  fcnvgreu  31898  ffsrn  31954  gsummpt2co  32200  tocycfvres1  32269  tocycfvres2  32270  cycpmfvlem  32271  cycpmfv3  32274  coinfliprv  33481  gg-icchmeo  35170  itg2addnclem2  36540  rncnv  37169  lnmlmic  41830  dmnonrel  42341  cnvrcl0  42376  conrel1d  42414