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

Theorem dfdm4 5049
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 2946 . . . . 5  |-  y  e. 
_V
2 vex 2946 . . . . 5  |-  x  e. 
_V
31, 2brcnv 5041 . . . 4  |-  ( y `' A x  <->  x A
y )
43exbii 1592 . . 3  |-  ( E. y  y `' A x 
<->  E. y  x A y )
54abbii 2542 . 2  |-  { x  |  E. y  y `' A x }  =  { x  |  E. y  x A y }
6 dfrn2 5045 . 2  |-  ran  `' A  =  { x  |  E. y  y `' A x }
7 df-dm 4874 . 2  |-  dom  A  =  { x  |  E. y  x A y }
85, 6, 73eqtr4ri 2461 1  |-  dom  A  =  ran  `' A
Colors of variables: wff set class
Syntax hints:   E.wex 1550    = wceq 1652   {cab 2416   class class class wbr 4199   `'ccnv 4863   dom cdm 4864   ran crn 4865
This theorem is referenced by:  dmcnvcnv  5078  rncnvcnv  5079  rncoeq  5125  cnvimass  5210  cnvimarndm  5211  dminxp  5297  cnvsn0  5324  rnsnopg  5335  dmmpt  5351  dmco  5364  cores2  5368  cnvssrndm  5377  unidmrn  5385  dfdm2  5387  cnvexg  5391  funimacnv  5511  foimacnv  5678  funcocnv2  5686  fimacnv  5848  f1opw2  6284  tz7.48-3  6687  fopwdom  7202  sbthlem4  7206  fodomr  7244  f1opwfi  7396  zorn2lem4  8363  unbenlem  13259  pjdm  16917  paste  17341  hmeores  17786  icchmeo  18949  gsumpropd2lem  24203  coinfliprv  24723  itg2addnclem2  26198  funsnfsup  26675  lnmlmic  27096
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pr 4390
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-br 4200  df-opab 4254  df-cnv 4872  df-dm 4874  df-rn 4875
  Copyright terms: Public domain W3C validator