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 2605	. . . . 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 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 𝐹 → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∃!weu 2596  Vcvv 3455  ∅c0 4287   class class class wbr 5110  dom cdm 5663  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-dm 5673  df-iota 6494  df-fv 6546

This theorem is referenced 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  7095  funiunfv  7248  funeldmb  7359  ovprc  7450  oprssdm  7593  nssdmovg  7594  ndmovg  7595  1st2val  8015  2nd2val  8016  brovpreldm  8085  soseq  8156  smofvon2  8344  rdgsucmptnf  8417  frsucmptn  8427  brwitnlem  8493  undifixp  8933  r1tr  9749  rankvaln  9772  cardidm  9946  carden2a  9953  carden2b  9954  carddomi2  9957  sdomsdomcardi  9958  pm54.43lem  9987  alephcard  10055  alephnbtwn  10056  alephgeom  10067  cfub  10233  cardcf  10236  cflecard  10237  cfle  10238  cflim2  10248  cfidm  10260  itunisuc  10404  itunitc1  10405  ituniiun  10407  alephadd  10563  alephreg  10568  pwcfsdom  10569  cfpwsdom  10570  adderpq  10942  mulerpq  10943  uzssz  12884  ltweuz  13999  wrdsymb0  14588  lsw0  14604  swrd00  14684  swrd0  14698  pfx00  14714  pfx0  14715  sumz  15775  sumss  15777  sumnul  15813  prod1  16000  prodss  16003  divsfval  17602  cidpropd  17767  lubval  18411  glbval  18424  joinval  18432  meetval  18446  gsumpropd2lem  18738  mulgfval  19136  mpfrcl  22217  iscnp2  23377  setsmstopn  24616  tngtopn  24788  dvbsss  26042  perfdvf  26043  dchrrcl  27385  nofv  27802  ltsres  27807  noseponlem  27809  noextenddif  27813  noextendlt  27814  noextendgt  27815  nolesgn2ores  27817  nogesgn1ores  27819  fvnobday  27823  nosepdmlem  27828  nosepssdm  27831  nosupbnd1lem3  27855  nosupbnd1lem5  27857  nosupbnd2lem1  27860  noinfbnd1lem3  27870  noinfbnd1lem5  27872  noinfbnd2lem1  27875  newval  28009  leftval  28023  rightval  28024  lltr  28036  madess  28040  oldssmade  28041  oldss  28044  lrold  28071  structiedg0val  29353  snstriedgval  29369  rgrx0nd  29925  vsfval  30966  dmadjrnb  32239  hmdmadj  32273  r1wf  35470  rdgprc0  36264  fullfunfv  36420  linedegen  36616  bj-inftyexpitaudisj  37830  bj-inftyexpidisj  37835  bj-fvimacnv0  37911  dibvalrel  41918  dicvalrelN  41940  dihvalrel  42034  itgocn  43874  fpwfvss  44121  r1rankcld  44938  grur1cld  44939  uz0  46109  climfveq  46366  climfveqf  46377  afv2ndeffv0  47980  fvmptrabdm  48013  fvconstr  49623  fvconstrn0  49624  fvconstr2  49625  fvconst0ci  49652  fvconstdomi  49653  ipolub00  49754  oppfrcl  49889  initopropdlemlem  50000  initopropd  50004  termopropd  50005  zeroopropd  50006  fucofvalne  50086