Theorem ndmfv 6915

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 2603	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5880	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 249	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 153	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6870	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 36	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6875	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 26	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 184	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∃!weu 2594  Vcvv 3451  ∅c0 4279   class class class wbr 5103  dom cdm 5651  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-dm 5661  df-iota 6493  df-fv 6545

This theorem is used by:  ndmfvrcl  6916  elfvdm  6917  nfvres  6921  fvfundmfvn0  6923  0fv  6924  funfv  6970  fvun1  6974  fvco4i  6985  fvmpti  6990  mptrcl  7001  fvmptss  7004  fvmptex  7006  fvmptnf  7014  fvmptss2  7018  elfvmptrab1  7020  fvopab4ndm  7022  f0cli  7096  fvtp0  7204  funiunfv  7250  funeldmb  7367  ovprc  7456  oprssdm  7600  nssdmovg  7601  ndmovg  7602  1st2val  8027  2nd2val  8028  brovpreldm  8098  soseq  8169  smofvon2  8357  rdgsucmptnf  8430  frsucmptn  8440  brwitnlem  8508  undifixp  8955  r1tr  9776  rankvaln  9800  r1wf  9834  cardidm  10033  carden2a  10040  carden2b  10041  carddomi2  10044  sdomsdomcardi  10045  pm54.43lem  10074  alephcard  10142  alephnbtwn  10143  alephgeom  10154  cfub  10319  cardcf  10322  cflecard  10323  cfle  10324  cflim2  10334  cfidm  10346  itunisuc  10490  itunitc1  10491  ituniiun  10493  alephadd  10655  alephreg  10660  pwcfsdom  10661  cfpwsdom  10662  adderpq  11034  mulerpq  11035  uzssz  12979  ltweuz  14097  wrdsymb0  14687  lsw0  14703  swrd00  14785  swrd0  14801  pfx00  14817  pfx0  14818  sumz  15881  sumss  15883  sumnul  15919  prod1  16104  prodss  16107  divsfval  17712  cidpropd  17877  lubval  18521  glbval  18534  joinval  18542  meetval  18556  gsumpropd2lem  18861  mulgfval  19272  mpfrcl  22387  iscnp2  23550  setsmstopn  24790  tngtopn  24962  dvbsss  26215  perfdvf  26216  dchrrcl  27560  nofv  28007  ltsres  28012  noseponlem  28014  noextenddif  28018  noextendlt  28019  noextendgt  28020  nolesgn2ores  28022  nogesgn1ores  28024  fvnobday  28028  nosepdmlem  28033  nosepssdm  28036  nosupbnd1lem3  28060  nosupbnd1lem5  28062  nosupbnd2lem1  28065  noinfbnd1lem3  28075  noinfbnd1lem5  28077  noinfbnd2lem1  28080  newval  28214  leftval  28228  rightval  28229  lltr  28241  madess  28245  oldssmade  28246  oldss  28249  lrold  28276  structiedg0val  29593  snstriedgval  29609  rgrx0nd  30168  vsfval  31228  dmadjrnb  32501  hmdmadj  32535  rdgprc0  36535  fullfunfv  36691  linedegen  36888  bj-inftyexpitaudisj  38106  bj-inftyexpidisj  38111  bj-fvimacnv0  38187  dibvalrel  42200  dicvalrelN  42222  dihvalrel  42316  itgocn  44150  fpwfvss  44397  r1rankcld  45214  grur1cld  45215  uz0  46391  climfveq  46648  climfveqf  46659  afv2ndeffv0  48299  fvmptrabdm  48332  ovconstbrd  49941  ovconstbrn0d  49942  elovconstbrd  49943  fvconst0ci  49968  fvconstdomi  49969  ipolub00  50070  oppfrcl  50205  initopropdlemlem  50316  initopropd  50320  termopropd  50321  zeroopropd  50322  fucofvalne  50402