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

Theorem ndmfv 6017
Description: The value of a class outside its domain is the empty set. (Contributed by NM, 24-Aug-1995.)
Assertion
Ref Expression
ndmfv 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅)

Proof of Theorem ndmfv
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 euex 2386 . . . . 5 (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2 eldmg 5132 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
31, 2syl5ibr 234 . . . 4 (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥𝐴 ∈ dom 𝐹))
43con3d 146 . . 3 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5 tz6.12-2 5983 . . 3 (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹𝐴) = ∅)
64, 5syl6 34 . 2 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
7 fvprc 5986 . . 3 𝐴 ∈ V → (𝐹𝐴) = ∅)
87a1d 25 . 2 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
96, 8pm2.61i 174 1 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wex 1694  wcel 1938  ∃!weu 2362  Vcvv 3077  c0 3777   class class class wbr 4481  dom cdm 4932  cfv 5694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-nul 4616  ax-pow 4668
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-dm 4942  df-iota 5658  df-fv 5702
This theorem is referenced by:  ndmfvrcl  6018  elfvdm  6019  nfvres  6023  fvfundmfvn0  6025  0fv  6026  funfv  6064  fvun1  6068  fvco4i  6075  fvmpti  6079  mptrcl  6087  fvmptss  6090  fvmptex  6092  fvmptnf  6099  fvmptss2  6101  elfvmptrab1  6102  fvopab4ndm  6104  f0cli  6167  funiunfv  6292  ovprc  6463  oprssdm  6594  nssdmovg  6595  ndmovg  6596  1st2val  6965  2nd2val  6966  brovpreldm  7021  curry1val  7037  curry2val  7041  smofvon2  7220  rdgsucmptnf  7292  frsucmptn  7301  brwitnlem  7354  undifixp  7710  r1tr  8402  rankvaln  8425  cardidm  8548  carden2a  8555  carden2b  8556  carddomi2  8559  sdomsdomcardi  8560  pm54.43lem  8588  alephcard  8656  alephnbtwn  8657  alephgeom  8668  cfub  8834  cardcf  8837  cflecard  8838  cfle  8839  cflim2  8848  cfidm  8860  itunisuc  9004  itunitc1  9005  ituniiun  9007  alephadd  9158  alephreg  9163  pwcfsdom  9164  cfpwsdom  9165  adderpq  9537  mulerpq  9538  uzssz  11451  ltweuz  12494  wrdsymb0  13057  lsw0  13068  swrd00  13133  swrd0  13149  sumz  14173  sumss  14175  sumnul  14206  prod1  14386  prodss  14389  divsfval  15926  cidpropd  16089  arwval  16412  coafval  16433  lubval  16703  glbval  16716  joinval  16724  meetval  16738  gsumpropd2lem  16992  mpfrcl  19247  iscnp2  20760  setsmstopn  21999  tngtopn  22164  pcofval  22545  dvbsss  23351  perfdvf  23352  dchrrcl  24658  eleenn  25470  clwwlknprop  26042  2wlkonot3v  26144  2spthonot3v  26145  vsfval  26634  dmadjrnb  27941  hmdmadj  27975  rdgprc0  30789  soseq  30841  nofv  30893  sltres  30900  noseponlem  30904  bdayelon  30918  fvnobday  30920  fullfunfv  31063  linedegen  31259  bj-inftyexpidisj  32109  dibvalrel  35364  dicvalrelN  35386  dihvalrel  35480  itgocn  36654  climfveq  38640  pfx00  40159  pfx0  40160  structiedg0val  40364  snstriedgval  40378  rgrx0nd  40903
  Copyright terms: Public domain W3C validator