Theorem ndmfv 6863

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 2574	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5844	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 246	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6818	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6823	. . 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 2565  Vcvv 3437  ∅c0 4282   class class class wbr 5095  dom cdm 5621  ‘cfv 6489

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 2705  ax-nul 5248  ax-pr 5374

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-dm 5631  df-iota 6445  df-fv 6497

This theorem is referenced by:  ndmfvrcl  6864  elfvdm  6865  nfvres  6869  fvfundmfvn0  6871  0fv  6872  funfv  6918  fvun1  6922  fvco4i  6932  fvmpti  6937  mptrcl  6947  fvmptss  6950  fvmptex  6952  fvmptnf  6960  fvmptss2  6964  elfvmptrab1  6966  fvopab4ndm  6968  f0cli  7040  funiunfv  7191  funeldmb  7302  ovprc  7393  oprssdm  7536  nssdmovg  7537  ndmovg  7538  1st2val  7958  2nd2val  7959  brovpreldm  8028  soseq  8098  smofvon2  8285  rdgsucmptnf  8357  frsucmptn  8367  brwitnlem  8431  undifixp  8868  r1tr  9680  rankvaln  9703  cardidm  9863  carden2a  9870  carden2b  9871  carddomi2  9874  sdomsdomcardi  9875  pm54.43lem  9904  alephcard  9972  alephnbtwn  9973  alephgeom  9984  cfub  10151  cardcf  10154  cflecard  10155  cfle  10156  cflim2  10165  cfidm  10177  itunisuc  10321  itunitc1  10322  ituniiun  10324  alephadd  10479  alephreg  10484  pwcfsdom  10485  cfpwsdom  10486  adderpq  10858  mulerpq  10859  uzssz  12763  ltweuz  13875  wrdsymb0  14463  lsw0  14479  swrd00  14559  swrd0  14573  pfx00  14589  pfx0  14590  sumz  15636  sumss  15638  sumnul  15674  prod1  15858  prodss  15861  divsfval  17459  cidpropd  17624  lubval  18268  glbval  18281  joinval  18289  meetval  18303  gsumpropd2lem  18595  mulgfval  18990  mpfrcl  22031  iscnp2  23174  setsmstopn  24413  tngtopn  24585  dvbsss  25850  perfdvf  25851  dchrrcl  27198  nofv  27616  sltres  27621  noseponlem  27623  noextenddif  27627  noextendlt  27628  noextendgt  27629  nolesgn2ores  27631  nogesgn1ores  27633  fvnobday  27637  nosepdmlem  27642  nosepssdm  27645  nosupbnd1lem3  27669  nosupbnd1lem5  27671  nosupbnd2lem1  27674  noinfbnd1lem3  27684  noinfbnd1lem5  27686  noinfbnd2lem1  27689  newval  27816  leftval  27824  rightval  27825  lltropt  27837  madess  27841  oldssmade  27842  oldss  27843  lrold  27862  structiedg0val  29021  snstriedgval  29037  rgrx0nd  29594  vsfval  30634  dmadjrnb  31907  hmdmadj  31941  r1wf  35179  rdgprc0  35907  fullfunfv  36063  linedegen  36259  bj-inftyexpitaudisj  37322  bj-inftyexpidisj  37327  bj-fvimacnv0  37403  dibvalrel  41335  dicvalrelN  41357  dihvalrel  41451  itgocn  43321  fpwfvss  43569  r1rankcld  44388  grur1cld  44389  uz0  45572  climfveq  45829  climfveqf  45840  afv2ndeffv0  47422  fvmptrabdm  47455  fvconstr  49023  fvconstrn0  49024  fvconstr2  49025  fvconst0ci  49052  fvconstdomi  49053  ipolub00  49154  oppfrcl  49289  initopropdlemlem  49400  initopropd  49404  termopropd  49405  zeroopropd  49406  fucofvalne  49486