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

Theorem ndmfv 5895
Description: The value of a class outside its domain is the empty set. (Contributed by NM, 24-Aug-1995.)
Assertion
Ref Expression
ndmfv

Proof of Theorem ndmfv
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 euex 2308 . . . . 5
2 eldmg 5203 . . . . 5
31, 2syl5ibr 221 . . . 4
43con3d 133 . . 3
5 tz6.12-2 5862 . . 3
64, 5syl6 33 . 2
7 fvprc 5865 . . 3
87a1d 25 . 2
96, 8pm2.61i 164 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  E.wex 1612  e.wcel 1818  E!weu 2282   cvv 3109   c0 3784   class class class wbr 4452  domcdm 5004  `cfv 5593
This theorem is referenced by:  ndmfvrcl  5896  elfvdm  5897  nfvres  5901  fvfundmfvn0  5903  0fv  5904  funfv  5940  fvun1  5944  fvco4i  5951  fvmpti  5955  fvmptss  5964  fvmptex  5966  fvmptnf  5973  fvmptss2  5975  elfvmptrab1  5976  fvopab4ndm  5978  f0cli  6042  funiunfv  6160  ovprc  6326  oprssdm  6456  nssdmovg  6457  ndmovg  6458  1st2val  6826  2nd2val  6827  bropopvvv  6880  curry1val  6893  curry2val  6897  smofvon2  7046  rdgsucmptnf  7114  frsucmptn  7123  brwitnlem  7176  undifixp  7525  r1tr  8215  rankvaln  8238  cardidm  8361  carden2a  8368  carden2b  8369  carddomi2  8372  sdomsdomcardi  8373  pm54.43lem  8401  alephcard  8472  alephnbtwn  8473  alephgeom  8484  cfub  8650  cardcf  8653  cflecard  8654  cfle  8655  cflim2  8664  cfidm  8676  itunisuc  8820  itunitc1  8821  ituniiun  8823  alephadd  8973  alephreg  8978  pwcfsdom  8979  cfpwsdom  8980  adderpq  9355  mulerpq  9356  uzssz  11129  ltweuz  12072  wrdsymb0  12575  lsw0  12586  swrd00  12645  swrd0  12658  sumz  13544  sumss  13546  sumnul  13575  prod1  13751  prodss  13754  divsfval  14944  cidpropd  15105  homarcl  15355  arwval  15370  coafval  15391  lubval  15614  glbval  15627  joinval  15635  meetval  15649  gsumpropd2lem  15900  mpfrcl  18187  iscnp2  19740  setsmstopn  20981  tngtopn  21164  pcofval  21510  dvbsss  22306  perfdvf  22307  dchrrcl  23515  eleenn  24199  clwwlknprop  24772  2wlkonot3v  24875  2spthonot3v  24876  vsfval  25528  dmadjrnb  26825  hmdmadj  26859  rdgprc0  29226  soseq  29334  nofv  29417  sltres  29424  bdayelon  29440  fvnobday  29442  fullfunfv  29597  linedegen  29793  itgocn  31113  mptrcl  32555  bj-inftyexpidisj  34613  dibvalrel  36890  dicvalrelN  36912  dihvalrel  37006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-nul 4581  ax-pow 4630
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-dm 5014  df-iota 5556  df-fv 5601
  Copyright terms: Public domain W3C validator