Theorem ndmfv 6942

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537  ∃wex 1776   ∈ wcel 2106  ∃!weu 2566  Vcvv 3478  ∅c0 4339   class class class wbr 5148  dom cdm 5689  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-dm 5699  df-iota 6516  df-fv 6571

This theorem is referenced by:  ndmfvrcl  6943  elfvdm  6944  nfvres  6948  fvfundmfvn0  6950  0fv  6951  funfv  6996  fvun1  7000  fvco4i  7010  fvmpti  7015  mptrcl  7025  fvmptss  7028  fvmptex  7030  fvmptnf  7038  fvmptss2  7042  elfvmptrab1  7044  fvopab4ndm  7046  f0cli  7118  funiunfv  7268  funeldmb  7379  ovprc  7469  oprssdm  7614  nssdmovg  7615  ndmovg  7616  1st2val  8041  2nd2val  8042  brovpreldm  8113  soseq  8183  smofvon2  8395  rdgsucmptnf  8468  frsucmptn  8478  brwitnlem  8544  undifixp  8973  r1tr  9814  rankvaln  9837  cardidm  9997  carden2a  10004  carden2b  10005  carddomi2  10008  sdomsdomcardi  10009  pm54.43lem  10038  alephcard  10108  alephnbtwn  10109  alephgeom  10120  cfub  10287  cardcf  10290  cflecard  10291  cfle  10292  cflim2  10301  cfidm  10313  itunisuc  10457  itunitc1  10458  ituniiun  10460  alephadd  10615  alephreg  10620  pwcfsdom  10621  cfpwsdom  10622  adderpq  10994  mulerpq  10995  uzssz  12897  ltweuz  13999  wrdsymb0  14584  lsw0  14600  swrd00  14679  swrd0  14693  pfx00  14709  pfx0  14710  sumz  15755  sumss  15757  sumnul  15793  prod1  15977  prodss  15980  divsfval  17594  cidpropd  17755  lubval  18414  glbval  18427  joinval  18435  meetval  18449  gsumpropd2lem  18705  mulgfval  19100  mpfrcl  22127  iscnp2  23263  setsmstopn  24506  tngtopn  24687  dvbsss  25952  perfdvf  25953  dchrrcl  27299  nofv  27717  sltres  27722  noseponlem  27724  noextenddif  27728  noextendlt  27729  noextendgt  27730  nolesgn2ores  27732  nogesgn1ores  27734  fvnobday  27738  nosepdmlem  27743  nosepssdm  27746  nosupbnd1lem3  27770  nosupbnd1lem5  27772  nosupbnd2lem1  27775  noinfbnd1lem3  27785  noinfbnd1lem5  27787  noinfbnd2lem1  27790  newval  27909  leftval  27917  rightval  27918  lltropt  27926  madess  27930  oldssmade  27931  lrold  27950  structiedg0val  29054  snstriedgval  29070  rgrx0nd  29627  vsfval  30662  dmadjrnb  31935  hmdmadj  31969  rdgprc0  35775  fullfunfv  35929  linedegen  36125  bj-inftyexpitaudisj  37188  bj-inftyexpidisj  37193  bj-fvimacnv0  37269  dibvalrel  41146  dicvalrelN  41168  dihvalrel  41262  itgocn  43153  fpwfvss  43402  r1rankcld  44227  grur1cld  44228  uz0  45362  climfveq  45625  climfveqf  45636  afv2ndeffv0  47210  fvmptrabdm  47243  fvconstr  48686  fvconstrn0  48687  fvconstr2  48688  fvconst0ci  48689  fvconstdomi  48690  ipolub00  48782