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

Theorem dfdm4 5738
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 3402 . . . . 5 𝑦 ∈ V
2 vex 3402 . . . . 5 𝑥 ∈ V
31, 2brcnv 5725 . . . 4 (𝑦𝐴𝑥𝑥𝐴𝑦)
43exbii 1854 . . 3 (∃𝑦 𝑦𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
54abbii 2803 . 2 {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6 dfrn2 5731 . 2 ran 𝐴 = {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥}
7 df-dm 5535 . 2 dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
85, 6, 73eqtr4ri 2772 1 dom 𝐴 = ran 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wex 1786  {cab 2716   class class class wbr 5030  ccnv 5524  dom cdm 5525  ran crn 5526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-dif 3846  df-un 3848  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031  df-opab 5093  df-cnv 5533  df-dm 5535  df-rn 5536
This theorem is referenced by:  dmcnvcnv  5776  rncnvcnv  5777  rncoeq  5818  cnvimass  5923  cnvimarndm  5924  dminxp  6012  cnvsn0  6042  rnsnopg  6053  dmmpt  6072  dmco  6087  cores2  6092  cnvssrndm  6103  unidmrn  6111  dfdm2  6113  funimacnv  6420  foimacnv  6635  funcocnv2  6642  fimacnvOLD  6848  f1opw2  7416  cnvexg  7655  tz7.48-3  8109  fopwdom  8674  sbthlem4  8680  fodomr  8718  cnvfi  8777  f1opwfi  8901  zorn2lem4  9999  trclublem  14444  relexpcnv  14484  unbenlem  16344  gsumpropd2lem  18005  pjdm  20523  paste  22045  hmeores  22522  icchmeo  23693  fcnvgreu  30585  ffsrn  30639  gsummpt2co  30885  tocycfvres1  30954  tocycfvres2  30955  cycpmfvlem  30956  cycpmfv3  30959  coinfliprv  32019  itg2addnclem2  35452  rncnv  36059  lnmlmic  40485  dmnonrel  40743  cnvrcl0  40778  conrel1d  40817
  Copyright terms: Public domain W3C validator