Theorem ndmfv 6914

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.

Step	Hyp	Ref	Expression
1		euex 2611	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5889	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 249	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 153	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6869	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 36	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6874	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 26	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 184	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567  ∃wex 1806   ∈ wcel 2149  ∃!weu 2602  Vcvv 3463  ∅c0 4294   class class class wbr 5113  dom cdm 5662  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-dm 5672  df-iota 6493  df-fv 6545

This theorem is referenced by:  ndmfvrcl  6915  elfvdm  6916  nfvres  6920  fvfundmfvn0  6922  0fv  6923  funfv  6969  fvun1  6973  fvco4i  6984  fvmpti  6989  mptrcl  7000  fvmptss  7003  fvmptex  7005  fvmptnf  7013  fvmptss2  7017  elfvmptrab1  7019  fvopab4ndm  7021  f0cli  7094  funiunfv  7247  funeldmb  7358  ovprc  7449  oprssdm  7592  nssdmovg  7593  ndmovg  7594  1st2val  8013  2nd2val  8014  brovpreldm  8083  soseq  8154  smofvon2  8342  rdgsucmptnf  8415  frsucmptn  8425  brwitnlem  8491  undifixp  8931  r1tr  9747  rankvaln  9770  cardidm  9944  carden2a  9951  carden2b  9952  carddomi2  9955  sdomsdomcardi  9956  pm54.43lem  9985  alephcard  10053  alephnbtwn  10054  alephgeom  10065  cfub  10231  cardcf  10234  cflecard  10235  cfle  10236  cflim2  10246  cfidm  10258  itunisuc  10402  itunitc1  10403  ituniiun  10405  alephadd  10561  alephreg  10566  pwcfsdom  10567  cfpwsdom  10568  adderpq  10940  mulerpq  10941  uzssz  12882  ltweuz  13996  wrdsymb0  14585  lsw0  14601  swrd00  14681  swrd0  14695  pfx00  14711  pfx0  14712  sumz  15772  sumss  15774  sumnul  15810  prod1  15997  prodss  16000  divsfval  17600  cidpropd  17765  lubval  18409  glbval  18422  joinval  18430  meetval  18444  gsumpropd2lem  18736  mulgfval  19134  mpfrcl  22204  iscnp2  23364  setsmstopn  24603  tngtopn  24775  dvbsss  26029  perfdvf  26030  dchrrcl  27369  nofv  27786  ltsres  27791  noseponlem  27793  noextenddif  27797  noextendlt  27798  noextendgt  27799  nolesgn2ores  27801  nogesgn1ores  27803  fvnobday  27807  nosepdmlem  27812  nosepssdm  27815  nosupbnd1lem3  27839  nosupbnd1lem5  27841  nosupbnd2lem1  27844  noinfbnd1lem3  27854  noinfbnd1lem5  27856  noinfbnd2lem1  27859  newval  27993  leftval  28007  rightval  28008  lltr  28020  madess  28024  oldssmade  28025  oldss  28028  lrold  28055  structiedg0val  29312  snstriedgval  29328  rgrx0nd  29884  vsfval  30925  dmadjrnb  32198  hmdmadj  32232  r1wf  35431  rdgprc0  36181  fullfunfv  36337  linedegen  36533  bj-inftyexpitaudisj  37736  bj-inftyexpidisj  37741  bj-fvimacnv0  37817  dibvalrel  41826  dicvalrelN  41848  dihvalrel  41942  itgocn  43782  fpwfvss  44029  r1rankcld  44846  grur1cld  44847  uz0  46017  climfveq  46274  climfveqf  46285  afv2ndeffv0  47885  fvmptrabdm  47918  fvconstr  49524  fvconstrn0  49525  fvconstr2  49526  fvconst0ci  49553  fvconstdomi  49554  ipolub00  49655  oppfrcl  49790  initopropdlemlem  49901  initopropd  49905  termopropd  49906  zeroopropd  49907  fucofvalne  49987