Theorem ndmfv 6911

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 5886	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 249	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 153	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6866	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 36	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6871	. . 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 5110  dom cdm 5659  ‘cfv 6533

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 5268  ax-pr 5402

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 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-dm 5669  df-iota 6489  df-fv 6541

This theorem is referenced by:  ndmfvrcl  6912  elfvdm  6913  nfvres  6917  fvfundmfvn0  6919  0fv  6920  funfv  6966  fvun1  6970  fvco4i  6981  fvmpti  6986  mptrcl  6997  fvmptss  7000  fvmptex  7002  fvmptnf  7010  fvmptss2  7014  elfvmptrab1  7016  fvopab4ndm  7018  f0cli  7091  funiunfv  7244  funeldmb  7355  ovprc  7446  oprssdm  7589  nssdmovg  7590  ndmovg  7591  1st2val  8010  2nd2val  8011  brovpreldm  8080  soseq  8151  smofvon2  8339  rdgsucmptnf  8412  frsucmptn  8422  brwitnlem  8488  undifixp  8928  r1tr  9744  rankvaln  9767  cardidm  9941  carden2a  9948  carden2b  9949  carddomi2  9952  sdomsdomcardi  9953  pm54.43lem  9982  alephcard  10050  alephnbtwn  10051  alephgeom  10062  cfub  10228  cardcf  10231  cflecard  10232  cfle  10233  cflim2  10243  cfidm  10255  itunisuc  10399  itunitc1  10400  ituniiun  10402  alephadd  10558  alephreg  10563  pwcfsdom  10564  cfpwsdom  10565  adderpq  10937  mulerpq  10938  uzssz  12879  ltweuz  13993  wrdsymb0  14582  lsw0  14598  swrd00  14678  swrd0  14692  pfx00  14708  pfx0  14709  sumz  15769  sumss  15771  sumnul  15807  prod1  15994  prodss  15997  divsfval  17597  cidpropd  17762  lubval  18406  glbval  18419  joinval  18427  meetval  18441  gsumpropd2lem  18733  mulgfval  19131  mpfrcl  22201  iscnp2  23361  setsmstopn  24600  tngtopn  24772  dvbsss  26026  perfdvf  26027  dchrrcl  27366  nofv  27783  ltsres  27788  noseponlem  27790  noextenddif  27794  noextendlt  27795  noextendgt  27796  nolesgn2ores  27798  nogesgn1ores  27800  fvnobday  27804  nosepdmlem  27809  nosepssdm  27812  nosupbnd1lem3  27836  nosupbnd1lem5  27838  nosupbnd2lem1  27841  noinfbnd1lem3  27851  noinfbnd1lem5  27853  noinfbnd2lem1  27856  newval  27990  leftval  28004  rightval  28005  lltr  28017  madess  28021  oldssmade  28022  oldss  28025  lrold  28052  structiedg0val  29309  snstriedgval  29325  rgrx0nd  29881  vsfval  30922  dmadjrnb  32195  hmdmadj  32229  r1wf  35428  rdgprc0  36178  fullfunfv  36334  linedegen  36530  bj-inftyexpitaudisj  37732  bj-inftyexpidisj  37737  bj-fvimacnv0  37813  dibvalrel  41822  dicvalrelN  41844  dihvalrel  41938  itgocn  43776  fpwfvss  44023  r1rankcld  44840  grur1cld  44841  uz0  46011  climfveq  46268  climfveqf  46279  afv2ndeffv0  47879  fvmptrabdm  47912  fvconstr  49518  fvconstrn0  49519  fvconstr2  49520  fvconst0ci  49547  fvconstdomi  49548  ipolub00  49649  oppfrcl  49784  initopropdlemlem  49895  initopropd  49899  termopropd  49900  zeroopropd  49901  fucofvalne  49981