Theorem ndmfv 6859

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∃!weu 2572  Vcvv 3431  ∅c0 4261   class class class wbr 5072  dom cdm 5618  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-dm 5628  df-iota 6441  df-fv 6493

This theorem is referenced by:  ndmfvrcl  6860  elfvdm  6861  nfvres  6865  fvfundmfvn0  6867  0fv  6868  funfv  6914  fvun1  6918  fvco4i  6929  fvmpti  6934  mptrcl  6945  fvmptss  6948  fvmptex  6950  fvmptnf  6958  fvmptss2  6962  elfvmptrab1  6964  fvopab4ndm  6966  f0cli  7039  funiunfv  7192  funeldmb  7303  ovprc  7394  oprssdm  7537  nssdmovg  7538  ndmovg  7539  1st2val  7959  2nd2val  7960  brovpreldm  8028  soseq  8099  smofvon2  8286  rdgsucmptnf  8358  frsucmptn  8368  brwitnlem  8432  undifixp  8872  r1tr  9691  rankvaln  9714  cardidm  9874  carden2a  9881  carden2b  9882  carddomi2  9885  sdomsdomcardi  9886  pm54.43lem  9915  alephcard  9983  alephnbtwn  9984  alephgeom  9995  cfub  10162  cardcf  10165  cflecard  10166  cfle  10167  cflim2  10176  cfidm  10188  itunisuc  10332  itunitc1  10333  ituniiun  10335  alephadd  10491  alephreg  10496  pwcfsdom  10497  cfpwsdom  10498  adderpq  10870  mulerpq  10871  uzssz  12800  ltweuz  13914  wrdsymb0  14502  lsw0  14518  swrd00  14598  swrd0  14612  pfx00  14628  pfx0  14629  sumz  15675  sumss  15677  sumnul  15713  prod1  15900  prodss  15903  divsfval  17502  cidpropd  17667  lubval  18311  glbval  18324  joinval  18332  meetval  18346  gsumpropd2lem  18638  mulgfval  19036  mpfrcl  22061  iscnp2  23222  setsmstopn  24461  tngtopn  24633  dvbsss  25887  perfdvf  25888  dchrrcl  27221  nofv  27639  ltsres  27644  noseponlem  27646  noextenddif  27650  noextendlt  27651  noextendgt  27652  nolesgn2ores  27654  nogesgn1ores  27656  fvnobday  27660  nosepdmlem  27665  nosepssdm  27668  nosupbnd1lem3  27692  nosupbnd1lem5  27694  nosupbnd2lem1  27697  noinfbnd1lem3  27707  noinfbnd1lem5  27709  noinfbnd2lem1  27712  newval  27845  leftval  27859  rightval  27860  lltr  27872  madess  27876  oldssmade  27877  oldss  27880  lrold  27907  structiedg0val  29109  snstriedgval  29125  rgrx0nd  29681  vsfval  30722  dmadjrnb  31995  hmdmadj  32029  r1wf  35277  rdgprc0  36019  fullfunfv  36175  linedegen  36371  bj-inftyexpitaudisj  37565  bj-inftyexpidisj  37570  bj-fvimacnv0  37646  dibvalrel  41655  dicvalrelN  41677  dihvalrel  41771  itgocn  43609  fpwfvss  43856  r1rankcld  44675  grur1cld  44676  uz0  45855  climfveq  46112  climfveqf  46123  afv2ndeffv0  47723  fvmptrabdm  47756  fvconstr  49352  fvconstrn0  49353  fvconstr2  49354  fvconst0ci  49381  fvconstdomi  49382  ipolub00  49483  oppfrcl  49618  initopropdlemlem  49729  initopropd  49733  termopropd  49734  zeroopropd  49735  fucofvalne  49815