MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfdm4 Structured version   Visualization version   GIF version

Theorem dfdm4 5851
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.
StepHypRef Expression
1 vex 3449 . . . . 5 𝑦 ∈ V
2 vex 3449 . . . . 5 𝑥 ∈ V
31, 2brcnv 5838 . . . 4 (𝑦𝐴𝑥𝑥𝐴𝑦)
43exbii 1850 . . 3 (∃𝑦 𝑦𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
54abbii 2806 . 2 {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6 dfrn2 5844 . 2 ran 𝐴 = {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥}
7 df-dm 5643 . 2 dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
85, 6, 73eqtr4ri 2775 1 dom 𝐴 = ran 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  wex 1781  {cab 2713   class class class wbr 5105  ccnv 5632  dom cdm 5633  ran crn 5634
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 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
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 2714  df-cleq 2728  df-clel 2814  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-br 5106  df-opab 5168  df-cnv 5641  df-dm 5643  df-rn 5644
This theorem is referenced by:  dmcnvcnv  5888  rncnvcnv  5889  rncoeq  5930  cnvimass  6033  cnvimarndm  6034  dminxp  6132  cnvsn0  6162  rnsnopg  6173  dmmpt  6192  dmco  6206  cores2  6211  cnvssrndm  6223  unidmrn  6231  dfdm2  6233  funimacnv  6582  foimacnv  6801  funcocnv2  6809  fimacnvOLD  7021  f1opw2  7608  cnvexg  7861  tz7.48-3  8390  fopwdom  9024  sbthlem4  9030  fodomr  9072  cnvfi  9124  f1opwfi  9300  zorn2lem4  10435  trclublem  14880  relexpcnv  14920  unbenlem  16780  gsumpropd2lem  18534  pjdm  21113  paste  22645  hmeores  23122  icchmeo  24304  fcnvgreu  31589  ffsrn  31646  gsummpt2co  31890  tocycfvres1  31959  tocycfvres2  31960  cycpmfvlem  31961  cycpmfv3  31964  coinfliprv  33082  itg2addnclem2  36130  rncnv  36761  lnmlmic  41401  dmnonrel  41852  cnvrcl0  41887  conrel1d  41925
  Copyright terms: Public domain W3C validator