Theorem ndmfv 6940

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539  ∃wex 1778   ∈ wcel 2107  ∃!weu 2567  Vcvv 3479  ∅c0 4332   class class class wbr 5142  dom cdm 5684  ‘cfv 6560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-dm 5694  df-iota 6513  df-fv 6568

This theorem is referenced by:  ndmfvrcl  6941  elfvdm  6942  nfvres  6946  fvfundmfvn0  6948  0fv  6949  funfv  6995  fvun1  6999  fvco4i  7009  fvmpti  7014  mptrcl  7024  fvmptss  7027  fvmptex  7029  fvmptnf  7037  fvmptss2  7041  elfvmptrab1  7043  fvopab4ndm  7045  f0cli  7117  funiunfv  7269  funeldmb  7380  ovprc  7470  oprssdm  7615  nssdmovg  7616  ndmovg  7617  1st2val  8043  2nd2val  8044  brovpreldm  8115  soseq  8185  smofvon2  8397  rdgsucmptnf  8470  frsucmptn  8480  brwitnlem  8546  undifixp  8975  r1tr  9817  rankvaln  9840  cardidm  10000  carden2a  10007  carden2b  10008  carddomi2  10011  sdomsdomcardi  10012  pm54.43lem  10041  alephcard  10111  alephnbtwn  10112  alephgeom  10123  cfub  10290  cardcf  10293  cflecard  10294  cfle  10295  cflim2  10304  cfidm  10316  itunisuc  10460  itunitc1  10461  ituniiun  10463  alephadd  10618  alephreg  10623  pwcfsdom  10624  cfpwsdom  10625  adderpq  10997  mulerpq  10998  uzssz  12900  ltweuz  14003  wrdsymb0  14588  lsw0  14604  swrd00  14683  swrd0  14697  pfx00  14713  pfx0  14714  sumz  15759  sumss  15761  sumnul  15797  prod1  15981  prodss  15984  divsfval  17593  cidpropd  17754  lubval  18402  glbval  18415  joinval  18423  meetval  18437  gsumpropd2lem  18693  mulgfval  19088  mpfrcl  22110  iscnp2  23248  setsmstopn  24491  tngtopn  24672  dvbsss  25938  perfdvf  25939  dchrrcl  27285  nofv  27703  sltres  27708  noseponlem  27710  noextenddif  27714  noextendlt  27715  noextendgt  27716  nolesgn2ores  27718  nogesgn1ores  27720  fvnobday  27724  nosepdmlem  27729  nosepssdm  27732  nosupbnd1lem3  27756  nosupbnd1lem5  27758  nosupbnd2lem1  27761  noinfbnd1lem3  27771  noinfbnd1lem5  27773  noinfbnd2lem1  27776  newval  27895  leftval  27903  rightval  27904  lltropt  27912  madess  27916  oldssmade  27917  lrold  27936  structiedg0val  29040  snstriedgval  29056  rgrx0nd  29613  vsfval  30653  dmadjrnb  31926  hmdmadj  31960  rdgprc0  35795  fullfunfv  35949  linedegen  36145  bj-inftyexpitaudisj  37207  bj-inftyexpidisj  37212  bj-fvimacnv0  37288  dibvalrel  41166  dicvalrelN  41188  dihvalrel  41282  itgocn  43181  fpwfvss  43430  r1rankcld  44255  grur1cld  44256  uz0  45428  climfveq  45689  climfveqf  45700  afv2ndeffv0  47277  fvmptrabdm  47310  fvconstr  48770  fvconstrn0  48771  fvconstr2  48772  fvconst0ci  48796  fvconstdomi  48797  ipolub00  48897  fucofvalne  49043