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

Theorem ndmfv 6113
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 2481 . . . . 5 (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2 eldmg 5228 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
31, 2syl5ibr 234 . . . 4 (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥𝐴 ∈ dom 𝐹))
43con3d 146 . . 3 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5 tz6.12-2 6079 . . 3 (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹𝐴) = ∅)
64, 5syl6 34 . 2 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
7 fvprc 6082 . . 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 1976  ∃!weu 2457  Vcvv 3172  c0 3873   class class class wbr 4577  dom cdm 5028  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-nul 4712  ax-pow 4764
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 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-dm 5038  df-iota 5754  df-fv 5798
This theorem is referenced by:  ndmfvrcl  6114  elfvdm  6115  nfvres  6119  fvfundmfvn0  6121  0fv  6122  funfv  6160  fvun1  6164  fvco4i  6171  fvmpti  6175  mptrcl  6183  fvmptss  6186  fvmptex  6188  fvmptnf  6195  fvmptss2  6197  elfvmptrab1  6198  fvopab4ndm  6200  f0cli  6263  funiunfv  6388  ovprc  6559  oprssdm  6690  nssdmovg  6691  ndmovg  6692  1st2val  7062  2nd2val  7063  brovpreldm  7118  curry1val  7134  curry2val  7138  smofvon2  7317  rdgsucmptnf  7389  frsucmptn  7398  brwitnlem  7451  undifixp  7807  r1tr  8499  rankvaln  8522  cardidm  8645  carden2a  8652  carden2b  8653  carddomi2  8656  sdomsdomcardi  8657  pm54.43lem  8685  alephcard  8753  alephnbtwn  8754  alephgeom  8765  cfub  8931  cardcf  8934  cflecard  8935  cfle  8936  cflim2  8945  cfidm  8957  itunisuc  9101  itunitc1  9102  ituniiun  9104  alephadd  9255  alephreg  9260  pwcfsdom  9261  cfpwsdom  9262  adderpq  9634  mulerpq  9635  uzssz  11539  ltweuz  12577  wrdsymb0  13140  lsw0  13151  swrd00  13216  swrd0  13232  sumz  14246  sumss  14248  sumnul  14279  prod1  14459  prodss  14462  divsfval  15976  cidpropd  16139  arwval  16462  coafval  16483  lubval  16753  glbval  16766  joinval  16774  meetval  16788  gsumpropd2lem  17042  mpfrcl  19285  iscnp2  20795  setsmstopn  22034  tngtopn  22202  pcofval  22549  dvbsss  23389  perfdvf  23390  dchrrcl  24682  eleenn  25494  clwwlknprop  26066  2wlkonot3v  26168  2spthonot3v  26169  vsfval  26658  dmadjrnb  27955  hmdmadj  27989  rdgprc0  30749  soseq  30801  nofv  30860  sltres  30867  noseponlem  30871  bdayelon  30885  fvnobday  30887  fullfunfv  31030  linedegen  31226  bj-inftyexpidisj  32077  dibvalrel  35273  dicvalrelN  35295  dihvalrel  35389  itgocn  36556  climfveq  38540  pfx00  40052  pfx0  40053  structiedg0val  40257  snstriedgval  40271  rgrx0nd  40796
  Copyright terms: Public domain W3C validator