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

Theorem dfdm4 5186
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 3109 . . . . 5  |-  y  e. 
_V
2 vex 3109 . . . . 5  |-  x  e. 
_V
31, 2brcnv 5176 . . . 4  |-  ( y `' A x  <->  x A
y )
43exbii 1639 . . 3  |-  ( E. y  y `' A x 
<->  E. y  x A y )
54abbii 2594 . 2  |-  { x  |  E. y  y `' A x }  =  { x  |  E. y  x A y }
6 dfrn2 5182 . 2  |-  ran  `' A  =  { x  |  E. y  y `' A x }
7 df-dm 5002 . 2  |-  dom  A  =  { x  |  E. y  x A y }
85, 6, 73eqtr4ri 2500 1  |-  dom  A  =  ran  `' A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374   E.wex 1591   {cab 2445   class class class wbr 4440   `'ccnv 4991   dom cdm 4992   ran crn 4993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-cnv 5000  df-dm 5002  df-rn 5003
This theorem is referenced by:  dmcnvcnv  5216  rncnvcnv  5217  rncoeq  5257  cnvimass  5348  cnvimarndm  5349  dminxp  5438  cnvsn0  5467  rnsnopg  5478  dmmpt  5493  dmco  5506  cores2  5511  cnvssrndm  5520  unidmrn  5528  dfdm2  5530  funimacnv  5651  foimacnv  5824  funcocnv2  5831  fimacnv  6004  f1opw2  6503  cnvexg  6720  tz7.48-3  7099  fopwdom  7615  sbthlem4  7620  fodomr  7658  f1opwfi  7813  zorn2lem4  8868  unbenlem  14274  gsumpropd2lem  15811  funsnfsupOLD  18020  pjdm  18498  paste  19554  hmeores  20000  icchmeo  21169  fcnvgreu  27172  ffsrn  27210  gsummpt2co  27420  coinfliprv  28047  itg2addnclem2  29631  lnmlmic  30627  conrel1d  36656  trclubg  36670
  Copyright terms: Public domain W3C validator