Theorem ndmfv 6866

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 2577	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5847	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 246	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6821	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6826	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 25	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 182	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∃!weu 2568  Vcvv 3440  ∅c0 4285   class class class wbr 5098  dom cdm 5624  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-dm 5634  df-iota 6448  df-fv 6500

This theorem is referenced by:  ndmfvrcl  6867  elfvdm  6868  nfvres  6872  fvfundmfvn0  6874  0fv  6875  funfv  6921  fvun1  6925  fvco4i  6935  fvmpti  6940  mptrcl  6950  fvmptss  6953  fvmptex  6955  fvmptnf  6963  fvmptss2  6967  elfvmptrab1  6969  fvopab4ndm  6971  f0cli  7043  funiunfv  7194  funeldmb  7305  ovprc  7396  oprssdm  7539  nssdmovg  7540  ndmovg  7541  1st2val  7961  2nd2val  7962  brovpreldm  8031  soseq  8101  smofvon2  8288  rdgsucmptnf  8360  frsucmptn  8370  brwitnlem  8434  undifixp  8872  r1tr  9688  rankvaln  9711  cardidm  9871  carden2a  9878  carden2b  9879  carddomi2  9882  sdomsdomcardi  9883  pm54.43lem  9912  alephcard  9980  alephnbtwn  9981  alephgeom  9992  cfub  10159  cardcf  10162  cflecard  10163  cfle  10164  cflim2  10173  cfidm  10185  itunisuc  10329  itunitc1  10330  ituniiun  10332  alephadd  10488  alephreg  10493  pwcfsdom  10494  cfpwsdom  10495  adderpq  10867  mulerpq  10868  uzssz  12772  ltweuz  13884  wrdsymb0  14472  lsw0  14488  swrd00  14568  swrd0  14582  pfx00  14598  pfx0  14599  sumz  15645  sumss  15647  sumnul  15683  prod1  15867  prodss  15870  divsfval  17468  cidpropd  17633  lubval  18277  glbval  18290  joinval  18298  meetval  18312  gsumpropd2lem  18604  mulgfval  18999  mpfrcl  22040  iscnp2  23183  setsmstopn  24422  tngtopn  24594  dvbsss  25859  perfdvf  25860  dchrrcl  27207  nofv  27625  ltsres  27630  noseponlem  27632  noextenddif  27636  noextendlt  27637  noextendgt  27638  nolesgn2ores  27640  nogesgn1ores  27642  fvnobday  27646  nosepdmlem  27651  nosepssdm  27654  nosupbnd1lem3  27678  nosupbnd1lem5  27680  nosupbnd2lem1  27683  noinfbnd1lem3  27693  noinfbnd1lem5  27695  noinfbnd2lem1  27698  newval  27831  leftval  27845  rightval  27846  lltr  27858  madess  27862  oldssmade  27863  oldss  27866  lrold  27893  structiedg0val  29095  snstriedgval  29111  rgrx0nd  29668  vsfval  30708  dmadjrnb  31981  hmdmadj  32015  r1wf  35252  rdgprc0  35985  fullfunfv  36141  linedegen  36337  bj-inftyexpitaudisj  37410  bj-inftyexpidisj  37415  bj-fvimacnv0  37491  dibvalrel  41423  dicvalrelN  41445  dihvalrel  41539  itgocn  43406  fpwfvss  43653  r1rankcld  44472  grur1cld  44473  uz0  45656  climfveq  45913  climfveqf  45924  afv2ndeffv0  47506  fvmptrabdm  47539  fvconstr  49107  fvconstrn0  49108  fvconstr2  49109  fvconst0ci  49136  fvconstdomi  49137  ipolub00  49238  oppfrcl  49373  initopropdlemlem  49484  initopropd  49488  termopropd  49489  zeroopropd  49490  fucofvalne  49570