Theorem ndmfv 6917

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 2607	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5890	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 249	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 153	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6872	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 36	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6877	. . 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 2146  ∃!weu 2598  Vcvv 3457  ∅c0 4286   class class class wbr 5111  dom cdm 5663  ‘cfv 6540

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 2148  ax-9 2156  ax-ext 2737  ax-nul 5271  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-dm 5673  df-iota 6496  df-fv 6548

This theorem is used by:  ndmfvrcl  6918  elfvdm  6919  nfvres  6923  fvfundmfvn0  6925  0fv  6926  funfv  6972  fvun1  6976  fvco4i  6987  fvmpti  6992  mptrcl  7003  fvmptss  7006  fvmptex  7008  fvmptnf  7016  fvmptss2  7020  elfvmptrab1  7022  fvopab4ndm  7024  f0cli  7097  funiunfv  7248  funeldmb  7365  ovprc  7454  oprssdm  7597  nssdmovg  7598  ndmovg  7599  1st2val  8016  2nd2val  8017  brovpreldm  8086  soseq  8157  smofvon2  8345  rdgsucmptnf  8418  frsucmptn  8428  brwitnlem  8494  undifixp  8934  r1tr  9751  rankvaln  9774  cardidm  9957  carden2a  9964  carden2b  9965  carddomi2  9968  sdomsdomcardi  9969  pm54.43lem  9998  alephcard  10066  alephnbtwn  10067  alephgeom  10078  cfub  10243  cardcf  10246  cflecard  10247  cfle  10248  cflim2  10258  cfidm  10270  itunisuc  10414  itunitc1  10415  ituniiun  10417  alephadd  10573  alephreg  10578  pwcfsdom  10579  cfpwsdom  10580  adderpq  10952  mulerpq  10953  uzssz  12894  ltweuz  14010  wrdsymb0  14599  lsw0  14615  swrd00  14697  swrd0  14713  pfx00  14729  pfx0  14730  sumz  15791  sumss  15793  sumnul  15829  prod1  16016  prodss  16019  divsfval  17618  cidpropd  17783  lubval  18427  glbval  18440  joinval  18448  meetval  18462  gsumpropd2lem  18758  mulgfval  19158  mpfrcl  22265  iscnp2  23425  setsmstopn  24664  tngtopn  24836  dvbsss  26090  perfdvf  26091  dchrrcl  27433  nofv  27850  ltsres  27855  noseponlem  27857  noextenddif  27861  noextendlt  27862  noextendgt  27863  nolesgn2ores  27865  nogesgn1ores  27867  fvnobday  27871  nosepdmlem  27876  nosepssdm  27879  nosupbnd1lem3  27903  nosupbnd1lem5  27905  nosupbnd2lem1  27908  noinfbnd1lem3  27918  noinfbnd1lem5  27920  noinfbnd2lem1  27923  newval  28057  leftval  28071  rightval  28072  lltr  28084  madess  28088  oldssmade  28089  oldss  28092  lrold  28119  structiedg0val  29401  snstriedgval  29417  rgrx0nd  29973  vsfval  31014  dmadjrnb  32287  hmdmadj  32321  r1wf  35506  rdgprc0  36296  fullfunfv  36452  linedegen  36648  bj-inftyexpitaudisj  37882  bj-inftyexpidisj  37887  bj-fvimacnv0  37963  dibvalrel  41970  dicvalrelN  41992  dihvalrel  42086  itgocn  43924  fpwfvss  44171  r1rankcld  44988  grur1cld  44989  uz0  46159  climfveq  46416  climfveqf  46427  afv2ndeffv0  48030  fvmptrabdm  48063  fvconstr  49673  fvconstrn0  49674  fvconstr2  49675  fvconst0ci  49702  fvconstdomi  49703  ipolub00  49804  oppfrcl  49939  initopropdlemlem  50050  initopropd  50054  termopropd  50055  zeroopropd  50056  fucofvalne  50136