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

Theorem imadmrn 5282
Description: The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
imadmrn  |-  ( A
" dom  A )  =  ran  A

Proof of Theorem imadmrn
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3075 . . . . . . 7  |-  x  e. 
_V
2 vex 3075 . . . . . . 7  |-  y  e. 
_V
31, 2opeldm 5146 . . . . . 6  |-  ( <.
x ,  y >.  e.  A  ->  x  e. 
dom  A )
43pm4.71i 632 . . . . 5  |-  ( <.
x ,  y >.  e.  A  <->  ( <. x ,  y >.  e.  A  /\  x  e.  dom  A ) )
5 ancom 450 . . . . 5  |-  ( (
<. x ,  y >.  e.  A  /\  x  e.  dom  A )  <->  ( x  e.  dom  A  /\  <. x ,  y >.  e.  A
) )
64, 5bitr2i 250 . . . 4  |-  ( ( x  e.  dom  A  /\  <. x ,  y
>.  e.  A )  <->  <. x ,  y >.  e.  A
)
76exbii 1635 . . 3  |-  ( E. x ( x  e. 
dom  A  /\  <. x ,  y >.  e.  A
)  <->  E. x <. x ,  y >.  e.  A
)
87abbii 2586 . 2  |-  { y  |  E. x ( x  e.  dom  A  /\  <. x ,  y
>.  e.  A ) }  =  { y  |  E. x <. x ,  y >.  e.  A }
9 dfima3 5275 . 2  |-  ( A
" dom  A )  =  { y  |  E. x ( x  e. 
dom  A  /\  <. x ,  y >.  e.  A
) }
10 dfrn3 5132 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
118, 9, 103eqtr4i 2491 1  |-  ( A
" dom  A )  =  ran  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1370   E.wex 1587    e. wcel 1758   {cab 2437   <.cop 3986   dom cdm 4943   ran crn 4944   "cima 4946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-sep 4516  ax-nul 4524  ax-pr 4634
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-ral 2801  df-rex 2802  df-rab 2805  df-v 3074  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-sn 3981  df-pr 3983  df-op 3987  df-br 4396  df-opab 4454  df-xp 4949  df-cnv 4951  df-dm 4953  df-rn 4954  df-res 4955  df-ima 4956
This theorem is referenced by:  cnvimarndm  5293  foima  5728  f1imacnv  5760  fsn2  5987  resfunexg  6047  elunirnALT  6073  fnexALT  6648  uniqs2  7267  mapsn  7359  phplem4  7598  php3  7602  jech9.3  8127  fin4en1  8584  retopbas  20466  plyeq0  21807  rnelshi  25610
  Copyright terms: Public domain W3C validator