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

Theorem dfdm4 5752
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 3483 . . . . 5 𝑦 ∈ V
2 vex 3483 . . . . 5 𝑥 ∈ V
31, 2brcnv 5741 . . . 4 (𝑦𝐴𝑥𝑥𝐴𝑦)
43exbii 1849 . . 3 (∃𝑦 𝑦𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
54abbii 2889 . 2 {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6 dfrn2 5747 . 2 ran 𝐴 = {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥}
7 df-dm 5553 . 2 dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
85, 6, 73eqtr4ri 2858 1 dom 𝐴 = ran 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wex 1781  {cab 2802   class class class wbr 5053  ccnv 5542  dom cdm 5543  ran crn 5544
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pr 5318
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-v 3482  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-br 5054  df-opab 5116  df-cnv 5551  df-dm 5553  df-rn 5554
This theorem is referenced by:  dmcnvcnv  5791  rncnvcnv  5792  rncoeq  5834  cnvimass  5937  cnvimarndm  5938  dminxp  6025  cnvsn0  6055  rnsnopg  6066  dmmpt  6082  dmco  6095  cores2  6100  cnvssrndm  6110  unidmrn  6118  dfdm2  6120  funimacnv  6424  foimacnv  6621  funcocnv2  6628  fimacnv  6828  f1opw2  7391  cnvexg  7621  tz7.48-3  8072  fopwdom  8617  sbthlem4  8623  fodomr  8661  f1opwfi  8821  zorn2lem4  9915  trclublem  14353  relexpcnv  14392  unbenlem  16240  gsumpropd2lem  17887  pjdm  20846  paste  21897  hmeores  22374  icchmeo  23544  fcnvgreu  30424  ffsrn  30471  gsummpt2co  30713  tocycfvres1  30779  tocycfvres2  30780  cycpmfvlem  30781  cycpmfv3  30784  coinfliprv  31767  itg2addnclem2  35021  rncnv  35630  lnmlmic  39888  dmnonrel  40146  cnvrcl0  40181  conrel1d  40220
  Copyright terms: Public domain W3C validator