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

Theorem ndmfv 5952
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 2377 . . . . 5 (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2 eldmg 5078 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
31, 2syl5ibr 231 . . . 4 (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥𝐴 ∈ dom 𝐹))
43con3d 142 . . 3 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5 tz6.12-2 5918 . . 3 (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹𝐴) = ∅)
64, 5syl6 34 . 2 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
7 fvprc 5921 . . 3 𝐴 ∈ V → (𝐹𝐴) = ∅)
87a1d 25 . 2 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
96, 8pm2.61i 171 1 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1468  wex 1692  wcel 1937  ∃!weu 2353  Vcvv 3066  c0 3757   class class class wbr 4434  dom cdm 4880  cfv 5633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-nul 4567  ax-pow 4619
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-dm 4890  df-iota 5597  df-fv 5641
This theorem is referenced by:  ndmfvrcl  5953  elfvdm  5954  nfvres  5958  fvfundmfvn0  5960  0fv  5961  funfv  5999  fvun1  6003  fvco4i  6010  fvmpti  6014  mptrcl  6022  fvmptss  6025  fvmptex  6027  fvmptnf  6034  fvmptss2  6036  elfvmptrab1  6037  fvopab4ndm  6039  f0cli  6100  funiunfv  6224  ovprc  6394  oprssdm  6525  nssdmovg  6526  ndmovg  6527  1st2val  6896  2nd2val  6897  brovpreldm  6952  curry1val  6968  curry2val  6972  smofvon2  7152  rdgsucmptnf  7224  frsucmptn  7233  brwitnlem  7286  undifixp  7641  r1tr  8332  rankvaln  8355  cardidm  8478  carden2a  8485  carden2b  8486  carddomi2  8489  sdomsdomcardi  8490  pm54.43lem  8518  alephcard  8586  alephnbtwn  8587  alephgeom  8598  cfub  8764  cardcf  8767  cflecard  8768  cfle  8769  cflim2  8778  cfidm  8790  itunisuc  8934  itunitc1  8935  ituniiun  8937  alephadd  9087  alephreg  9092  pwcfsdom  9093  cfpwsdom  9094  adderpq  9466  mulerpq  9467  uzssz  11269  ltweuz  12288  wrdsymb0  12833  lsw0  12844  swrd00  12908  swrd0  12924  sumz  13948  sumss  13950  sumnul  13981  prod1  14158  prodss  14161  divsfval  15618  cidpropd  15781  arwval  16104  coafval  16125  lubval  16395  glbval  16408  joinval  16416  meetval  16430  gsumpropd2lem  16681  mpfrcl  18900  iscnp2  20412  setsmstopn  21651  tngtopn  21816  pcofval  22200  dvbsss  23018  perfdvf  23019  dchrrcl  24329  eleenn  25087  clwwlknprop  25661  2wlkonot3v  25763  2spthonot3v  25764  vsfval  26417  dmadjrnb  27722  hmdmadj  27756  rdgprc0  30591  soseq  30643  nofv  30695  sltres  30702  noseponlem  30706  bdayelon  30720  fvnobday  30722  fullfunfv  30865  linedegen  31061  bj-inftyexpidisj  31873  dibvalrel  34971  dicvalrelN  34993  dihvalrel  35087  itgocn  36270  pfx00  39447  pfx0  39448  structiedg0val  39655  snstriedgval  39669  rgrx0nd  40194
  Copyright terms: Public domain W3C validator