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

Theorem dfdm4 5185
Description: Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)
Assertion
Ref Expression
dfdm4  |-  dom  A  =  ran  `' A

Proof of Theorem dfdm4
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3098 . . . . 5  |-  y  e. 
_V
2 vex 3098 . . . . 5  |-  x  e. 
_V
31, 2brcnv 5175 . . . 4  |-  ( y `' A x  <->  x A
y )
43exbii 1654 . . 3  |-  ( E. y  y `' A x 
<->  E. y  x A y )
54abbii 2577 . 2  |-  { x  |  E. y  y `' A x }  =  { x  |  E. y  x A y }
6 dfrn2 5181 . 2  |-  ran  `' A  =  { x  |  E. y  y `' A x }
7 df-dm 4999 . 2  |-  dom  A  =  { x  |  E. y  x A y }
85, 6, 73eqtr4ri 2483 1  |-  dom  A  =  ran  `' A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383   E.wex 1599   {cab 2428   class class class wbr 4437   `'ccnv 4988   dom cdm 4989   ran crn 4990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-cnv 4997  df-dm 4999  df-rn 5000
This theorem is referenced by:  dmcnvcnv  5215  rncnvcnv  5216  rncoeq  5256  cnvimass  5347  cnvimarndm  5348  dminxp  5437  cnvsn0  5466  rnsnopg  5477  dmmpt  5492  dmco  5505  cores2  5510  cnvssrndm  5519  unidmrn  5527  dfdm2  5529  funimacnv  5650  foimacnv  5823  funcocnv2  5830  fimacnv  6004  f1opw2  6513  cnvexg  6731  tz7.48-3  7111  fopwdom  7627  sbthlem4  7632  fodomr  7670  f1opwfi  7826  zorn2lem4  8882  unbenlem  14303  gsumpropd2lem  15774  funsnfsupOLD  18130  pjdm  18611  paste  19668  hmeores  20145  icchmeo  21314  fcnvgreu  27386  ffsrn  27424  gsummpt2co  27644  coinfliprv  28294  itg2addnclem2  30042  lnmlmic  31009  conrel1d  37458  trclubg  37472
  Copyright terms: Public domain W3C validator