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

Theorem ndmfv 5709
 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 2275 . . . . 5
2 eldmg 5019 . . . . 5
31, 2syl5ibr 213 . . . 4
43con3d 127 . . 3
5 tz6.12-2 5673 . . 3
64, 5syl6 31 . 2
7 fvprc 5676 . . 3
87a1d 23 . 2
96, 8pm2.61i 158 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4  wex 1547   wceq 1649   wcel 1721  weu 2252  cvv 2913  c0 3585   class class class wbr 4167   cdm 4832  cfv 5408 This theorem is referenced by:  ndmfvrcl  5710  elfvdm  5711  nfvres  5714  fv01  5716  funfv  5743  fvun1  5747  fvco4i  5754  fvmpti  5758  fvmptss  5766  fvmptex  5768  fvmptnf  5775  fvmptss2  5777  fvopab4ndm  5778  f0cli  5833  funiunfv  5948  ovprc  6061  oprssdm  6181  nssdmovg  6182  ndmovg  6183  1st2val  6325  2nd2val  6326  bropopvvv  6379  curry1val  6392  curry2val  6396  smofvon2  6568  rdgsucmptnf  6637  frsucmptn  6646  brwitnlem  6701  undifixp  7048  r1tr  7649  rankvaln  7672  cardidm  7793  carden2a  7800  carden2b  7801  carddomi2  7804  sdomsdomcardi  7805  pm54.43lem  7833  alephcard  7898  alephnbtwn  7899  alephgeom  7910  cfub  8076  cardcf  8079  cflecard  8080  cfle  8081  cflim2  8090  cfidm  8102  itunisuc  8246  itunitc1  8247  ituniiun  8249  alephadd  8399  alephreg  8404  pwcfsdom  8405  cfpwsdom  8406  adderpq  8780  mulerpq  8781  uzssz  10451  ltweuz  11242  swrd00  11706  sumz  12457  sumss  12459  sumnul  12485  divsfval  13713  cidpropd  13877  homarcl  14124  arwval  14139  coafval  14160  iscnp2  17243  setsmstopn  18447  tngtopn  18630  pcofval  18974  dvbsss  19728  perfdvf  19729  mpfrcl  19878  dchrrcl  20963  vsfval  22034  dmadjrnb  23329  hmdmadj  23363  gsumpropd2lem  24142  prod1  25192  prodss  25195  rdgprc0  25333  soseq  25437  nofv  25494  sltres  25501  bdayelon  25517  fvnobday  25519  fullfunfv  25669  eleenn  25708  linedegen  25950  itgocn  27199  fvfundmfvn0  27817  2wlkonot3v  28012  2spthonot3v  28013  dibvalrel  31586  dicvalrelN  31608  dihvalrel  31702 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-nul 4293  ax-pow 4332 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-rab 2672  df-v 2915  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-nul 3586  df-if 3697  df-sn 3777  df-pr 3778  df-op 3780  df-uni 3972  df-br 4168  df-dm 4842  df-iota 5372  df-fv 5416
 Copyright terms: Public domain W3C validator