Theorem ndmfv 6918

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 2602	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5879	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 249	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 153	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6873	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 36	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6878	. . 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 1569  ∃wex 1811   ∈ wcel 2144  ∃!weu 2593  Vcvv 3450  ∅c0 4278   class class class wbr 5102  dom cdm 5650  ‘cfv 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-dm 5660  df-iota 6494  df-fv 6547

This theorem is used by:  ndmfvrcl  6919  elfvdm  6920  nfvres  6924  fvfundmfvn0  6926  0fv  6927  funfv  6973  fvun1  6977  fvco4i  6988  fvmpti  6993  mptrcl  7004  fvmptss  7007  fvmptex  7009  fvmptnf  7017  fvmptss2  7021  elfvmptrab1  7023  fvopab4ndm  7025  f0cli  7099  fvtp0  7207  funiunfv  7253  funeldmb  7370  ovprc  7459  oprssdm  7603  nssdmovg  7604  ndmovg  7605  1st2val  8030  2nd2val  8031  brovpreldm  8101  soseq  8179  smofvon2  8368  rdgsucmptnf  8441  frsucmptn  8451  brwitnlem  8519  undifixp  8966  r1tr  9787  rankvaln  9811  r1wf  9845  cardidm  10044  carden2a  10051  carden2b  10052  carddomi2  10055  sdomsdomcardi  10056  pm54.43lem  10085  alephcard  10153  alephnbtwn  10154  alephgeom  10165  cfub  10330  cardcf  10333  cflecard  10334  cfle  10335  cflim2  10345  cfidm  10357  itunisuc  10501  itunitc1  10502  ituniiun  10504  alephadd  10666  alephreg  10671  pwcfsdom  10672  cfpwsdom  10673  adderpq  11045  mulerpq  11046  uzssz  12990  ltweuz  14108  wrdsymb0  14698  lsw0  14714  swrd00  14797  swrd0  14813  pfx00  14829  pfx0  14830  sumz  15894  sumss  15896  sumnul  15932  prod1  16117  prodss  16120  divsfval  17725  cidpropd  17890  lubval  18534  glbval  18547  joinval  18555  meetval  18569  gsumpropd2lem  18874  mulgfval  19285  mpfrcl  22400  iscnp2  23563  setsmstopn  24803  tngtopn  24975  dvbsss  26228  perfdvf  26229  dchrrcl  27573  nofv  28020  ltsres  28025  noseponlem  28027  noextenddif  28031  noextendlt  28032  noextendgt  28033  nolesgn2ores  28035  nogesgn1ores  28037  fvnobday  28041  nosepdmlem  28046  nosepssdm  28049  nosupbnd1lem3  28073  nosupbnd1lem5  28075  nosupbnd2lem1  28078  noinfbnd1lem3  28088  noinfbnd1lem5  28090  noinfbnd2lem1  28093  newval  28227  leftval  28241  rightval  28242  lltr  28254  madess  28258  oldssmade  28259  oldss  28262  lrold  28289  structiedg0val  29606  snstriedgval  29622  rgrx0nd  30181  vsfval  31241  dmadjrnb  32514  hmdmadj  32548  acwer1prclem  35816  j0ltaleph  35948  rdgprc0  36648  fullfunfv  36804  linedegen  37001  bj-inftyexpitaudisj  38220  bj-inftyexpidisj  38225  bj-fvimacnv0  38301  dibvalrel  42314  dicvalrelN  42336  dihvalrel  42430  itgocn  44260  fpwfvss  44507  r1rankcld  45323  grur1cld  45324  uz0  46516  climfveq  46773  climfveqf  46784  afv2ndeffv0  48424  fvmptrabdm  48457  ovconstbrd  50067  ovconstbrn0d  50068  elovconstbrd  50069  fvconst0ci  50099  fvconstdomi  50100  ipolub00  50201  oppfrcl  50338  initopropdlemlem  50455  initopropd  50459  termopropd  50460  zeroopropd  50461  fucofvalne  50541