Theorem dfdm4 5893

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

Syntax hints:   = wceq 1541  ∃wex 1781  {cab 2709   class class class wbr 5147  ^◡ccnv 5674  dom cdm 5675  ran crn 5676

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-cnv 5683  df-dm 5685  df-rn 5686

This theorem is referenced by:  dmcnvcnv  5930  rncnvcnv  5931  rncoeq  5972  cnvimass  6077  cnvimarndm  6078  dminxp  6176  cnvsn0  6206  rnsnopg  6217  dmmpt  6236  dmco  6250  cores2  6255  cnvssrndm  6267  unidmrn  6275  dfdm2  6277  funimacnv  6626  foimacnv  6847  funcocnv2  6855  fimacnvOLD  7069  f1opw2  7657  cnvexg  7911  tz7.48-3  8440  fopwdom  9076  sbthlem4  9082  fodomr  9124  cnvfi  9176  f1opwfi  9352  zorn2lem4  10490  trclublem  14938  relexpcnv  14978  unbenlem  16837  gsumpropd2lem  18594  pjdm  21253  paste  22789  hmeores  23266  icchmeo  24448  fcnvgreu  31885  ffsrn  31941  gsummpt2co  32187  tocycfvres1  32256  tocycfvres2  32257  cycpmfvlem  32258  cycpmfv3  32261  coinfliprv  33469  gg-icchmeo  35158  itg2addnclem2  36528  rncnv  37157  lnmlmic  41815  dmnonrel  42326  cnvrcl0  42361  conrel1d  42399