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

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.
StepHypRef Expression
1 vex 3436 . . . . 5 𝑦 ∈ V
2 vex 3436 . . . . 5 𝑥 ∈ V
31, 2brcnv 5791 . . . 4 (𝑦𝐴𝑥𝑥𝐴𝑦)
43exbii 1850 . . 3 (∃𝑦 𝑦𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
54abbii 2808 . 2 {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6 dfrn2 5797 . 2 ran 𝐴 = {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥}
7 df-dm 5599 . 2 dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
85, 6, 73eqtr4ri 2777 1 dom 𝐴 = ran 𝐴
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator