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

Theorem dfdm4 5108
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 3037 . . . . 5  |-  y  e. 
_V
2 vex 3037 . . . . 5  |-  x  e. 
_V
31, 2brcnv 5098 . . . 4  |-  ( y `' A x  <->  x A
y )
43exbii 1675 . . 3  |-  ( E. y  y `' A x 
<->  E. y  x A y )
54abbii 2516 . 2  |-  { x  |  E. y  y `' A x }  =  { x  |  E. y  x A y }
6 dfrn2 5104 . 2  |-  ran  `' A  =  { x  |  E. y  y `' A x }
7 df-dm 4923 . 2  |-  dom  A  =  { x  |  E. y  x A y }
85, 6, 73eqtr4ri 2422 1  |-  dom  A  =  ran  `' A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1399   E.wex 1620   {cab 2367   class class class wbr 4367   `'ccnv 4912   dom cdm 4913   ran crn 4914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-opab 4426  df-cnv 4921  df-dm 4923  df-rn 4924
This theorem is referenced by:  dmcnvcnv  5138  rncnvcnv  5139  rncoeq  5179  cnvimass  5269  cnvimarndm  5270  dminxp  5357  cnvsn0  5384  rnsnopg  5395  dmmpt  5410  dmco  5423  cores2  5428  cnvssrndm  5437  unidmrn  5446  dfdm2  5448  funimacnv  5568  foimacnv  5741  funcocnv2  5748  fimacnv  5921  f1opw2  6427  cnvexg  6645  tz7.48-3  7027  fopwdom  7544  sbthlem4  7549  fodomr  7587  f1opwfi  7739  zorn2lem4  8792  trclublem  12833  relexpcnv  12870  unbenlem  14428  gsumpropd2lem  16017  funsnfsupOLD  18369  pjdm  18829  paste  19881  hmeores  20357  icchmeo  21526  fcnvgreu  27660  ffsrn  27702  gsummpt2co  27924  coinfliprv  28604  itg2addnclem2  30233  lnmlmic  31200  conrel1d  38192
  Copyright terms: Public domain W3C validator