Theorem ndmfv 6874

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃!weu 2569  Vcvv 3442  ∅c0 4287   class class class wbr 5100  dom cdm 5632  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-dm 5642  df-iota 6456  df-fv 6508

This theorem is referenced by:  ndmfvrcl  6875  elfvdm  6876  nfvres  6880  fvfundmfvn0  6882  0fv  6883  funfv  6929  fvun1  6933  fvco4i  6943  fvmpti  6948  mptrcl  6959  fvmptss  6962  fvmptex  6964  fvmptnf  6972  fvmptss2  6976  elfvmptrab1  6978  fvopab4ndm  6980  f0cli  7052  funiunfv  7204  funeldmb  7315  ovprc  7406  oprssdm  7549  nssdmovg  7550  ndmovg  7551  1st2val  7971  2nd2val  7972  brovpreldm  8041  soseq  8111  smofvon2  8298  rdgsucmptnf  8370  frsucmptn  8380  brwitnlem  8444  undifixp  8884  r1tr  9700  rankvaln  9723  cardidm  9883  carden2a  9890  carden2b  9891  carddomi2  9894  sdomsdomcardi  9895  pm54.43lem  9924  alephcard  9992  alephnbtwn  9993  alephgeom  10004  cfub  10171  cardcf  10174  cflecard  10175  cfle  10176  cflim2  10185  cfidm  10197  itunisuc  10341  itunitc1  10342  ituniiun  10344  alephadd  10500  alephreg  10505  pwcfsdom  10506  cfpwsdom  10507  adderpq  10879  mulerpq  10880  uzssz  12784  ltweuz  13896  wrdsymb0  14484  lsw0  14500  swrd00  14580  swrd0  14594  pfx00  14610  pfx0  14611  sumz  15657  sumss  15659  sumnul  15695  prod1  15879  prodss  15882  divsfval  17480  cidpropd  17645  lubval  18289  glbval  18302  joinval  18310  meetval  18324  gsumpropd2lem  18616  mulgfval  19011  mpfrcl  22052  iscnp2  23195  setsmstopn  24434  tngtopn  24606  dvbsss  25871  perfdvf  25872  dchrrcl  27219  nofv  27637  ltsres  27642  noseponlem  27644  noextenddif  27648  noextendlt  27649  noextendgt  27650  nolesgn2ores  27652  nogesgn1ores  27654  fvnobday  27658  nosepdmlem  27663  nosepssdm  27666  nosupbnd1lem3  27690  nosupbnd1lem5  27692  nosupbnd2lem1  27695  noinfbnd1lem3  27705  noinfbnd1lem5  27707  noinfbnd2lem1  27710  newval  27843  leftval  27857  rightval  27858  lltr  27870  madess  27874  oldssmade  27875  oldss  27878  lrold  27905  structiedg0val  29107  snstriedgval  29123  rgrx0nd  29680  vsfval  30721  dmadjrnb  31994  hmdmadj  32028  r1wf  35273  rdgprc0  36007  fullfunfv  36163  linedegen  36359  bj-inftyexpitaudisj  37460  bj-inftyexpidisj  37465  bj-fvimacnv0  37541  dibvalrel  41539  dicvalrelN  41561  dihvalrel  41655  itgocn  43521  fpwfvss  43768  r1rankcld  44587  grur1cld  44588  uz0  45770  climfveq  46027  climfveqf  46038  afv2ndeffv0  47620  fvmptrabdm  47653  fvconstr  49221  fvconstrn0  49222  fvconstr2  49223  fvconst0ci  49250  fvconstdomi  49251  ipolub00  49352  oppfrcl  49487  initopropdlemlem  49598  initopropd  49602  termopropd  49603  zeroopropd  49604  fucofvalne  49684