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

Theorem ndmfv 6694
Description: The value of a class outside its domain is the empty set. (An artifact of our function value definition.) (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 2658 . . . . 5 (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2 eldmg 5761 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
31, 2syl5ibr 247 . . . 4 (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥𝐴 ∈ dom 𝐹))
43con3d 155 . . 3 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5 tz6.12-2 6654 . . 3 (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹𝐴) = ∅)
64, 5syl6 35 . 2 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
7 fvprc 6657 . . 3 𝐴 ∈ V → (𝐹𝐴) = ∅)
87a1d 25 . 2 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
96, 8pm2.61i 183 1 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wex 1771  wcel 2105  ∃!weu 2649  Vcvv 3495  c0 4290   class class class wbr 5058  dom cdm 5549  cfv 6349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-nul 5202  ax-pow 5258
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-dm 5559  df-iota 6308  df-fv 6357
This theorem is referenced by:  ndmfvrcl  6695  elfvdm  6696  nfvres  6700  fvfundmfvn0  6702  0fv  6703  funfv  6744  fvun1  6748  fvco4i  6756  fvmpti  6761  mptrcl  6770  fvmptss  6773  fvmptex  6775  fvmptnf  6783  fvmptss2  6786  elfvmptrab1  6788  fvopab4ndm  6790  f0cli  6857  funiunfv  6998  ovprc  7183  oprssdm  7318  nssdmovg  7319  ndmovg  7320  1st2val  7708  2nd2val  7709  brovpreldm  7775  smofvon2  7984  rdgsucmptnf  8056  frsucmptn  8065  brwitnlem  8123  undifixp  8487  r1tr  9194  rankvaln  9217  cardidm  9377  carden2a  9384  carden2b  9385  carddomi2  9388  sdomsdomcardi  9389  pm54.43lem  9417  alephcard  9485  alephnbtwn  9486  alephgeom  9497  cfub  9660  cardcf  9663  cflecard  9664  cfle  9665  cflim2  9674  cfidm  9686  itunisuc  9830  itunitc1  9831  ituniiun  9833  alephadd  9988  alephreg  9993  pwcfsdom  9994  cfpwsdom  9995  adderpq  10367  mulerpq  10368  uzssz  12253  ltweuz  13319  wrdsymb0  13891  lsw0  13907  swrd00  13996  swrd0  14010  pfx00  14026  pfx0  14027  sumz  15069  sumss  15071  sumnul  15105  prod1  15288  prodss  15291  divsfval  16810  cidpropd  16970  lubval  17584  glbval  17597  joinval  17605  meetval  17619  gsumpropd2lem  17879  mulgfval  18166  mpfrcl  20228  iscnp2  21777  setsmstopn  23017  tngtopn  23188  dvbsss  24429  perfdvf  24430  dchrrcl  25744  structiedg0val  26735  snstriedgval  26751  rgrx0nd  27304  vsfval  28338  dmadjrnb  29611  hmdmadj  29645  funeldmb  32904  rdgprc0  32936  soseq  32994  nofv  33062  sltres  33067  noseponlem  33069  noextenddif  33073  noextendlt  33074  noextendgt  33075  nolesgn2ores  33077  fvnobday  33081  nosepdmlem  33085  nosepssdm  33088  nosupbnd1lem3  33108  nosupbnd1lem5  33110  nosupbnd2lem1  33113  fullfunfv  33306  linedegen  33502  bj-inftyexpitaudisj  34380  bj-inftyexpidisj  34385  bj-fvimacnv0  34457  dibvalrel  38181  dicvalrelN  38203  dihvalrel  38297  itgocn  39644  r1rankcld  40447  grur1cld  40448  uz0  41566  climfveq  41830  climfveqf  41841  afv2ndeffv0  43340  fvmptrabdm  43373  setrec2lem1  44694
  Copyright terms: Public domain W3C validator