Theorem ndmfv 6927

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 2572	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5899	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 245	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6880	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6884	. . 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 1782   ∈ wcel 2107  ∃!weu 2563  Vcvv 3475  ∅c0 4323   class class class wbr 5149  dom cdm 5677  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-dm 5687  df-iota 6496  df-fv 6552

This theorem is referenced by:  ndmfvrcl  6928  elfvdm  6929  nfvres  6933  fvfundmfvn0  6935  0fv  6936  funfv  6979  fvun1  6983  fvco4i  6993  fvmpti  6998  mptrcl  7008  fvmptss  7011  fvmptex  7013  fvmptnf  7021  fvmptss2  7024  elfvmptrab1  7026  fvopab4ndm  7028  f0cli  7100  funiunfv  7247  funeldmb  7356  ovprc  7447  oprssdm  7588  nssdmovg  7589  ndmovg  7590  1st2val  8003  2nd2val  8004  brovpreldm  8075  soseq  8145  smofvon2  8356  rdgsucmptnf  8429  frsucmptn  8439  brwitnlem  8507  undifixp  8928  r1tr  9771  rankvaln  9794  cardidm  9954  carden2a  9961  carden2b  9962  carddomi2  9965  sdomsdomcardi  9966  pm54.43lem  9995  alephcard  10065  alephnbtwn  10066  alephgeom  10077  cfub  10244  cardcf  10247  cflecard  10248  cfle  10249  cflim2  10258  cfidm  10270  itunisuc  10414  itunitc1  10415  ituniiun  10417  alephadd  10572  alephreg  10577  pwcfsdom  10578  cfpwsdom  10579  adderpq  10951  mulerpq  10952  uzssz  12843  ltweuz  13926  wrdsymb0  14499  lsw0  14515  swrd00  14594  swrd0  14608  pfx00  14624  pfx0  14625  sumz  15668  sumss  15670  sumnul  15706  prod1  15888  prodss  15891  divsfval  17493  cidpropd  17654  lubval  18309  glbval  18322  joinval  18330  meetval  18344  gsumpropd2lem  18598  mulgfval  18952  mpfrcl  21648  iscnp2  22743  setsmstopn  23986  tngtopn  24167  dvbsss  25419  perfdvf  25420  dchrrcl  26743  nofv  27160  sltres  27165  noseponlem  27167  noextenddif  27171  noextendlt  27172  noextendgt  27173  nolesgn2ores  27175  nogesgn1ores  27177  fvnobday  27181  nosepdmlem  27186  nosepssdm  27189  nosupbnd1lem3  27213  nosupbnd1lem5  27215  nosupbnd2lem1  27218  noinfbnd1lem3  27228  noinfbnd1lem5  27230  noinfbnd2lem1  27233  newval  27350  leftval  27358  rightval  27359  lltropt  27367  madess  27371  oldssmade  27372  lrold  27391  structiedg0val  28282  snstriedgval  28298  rgrx0nd  28851  vsfval  29886  dmadjrnb  31159  hmdmadj  31193  rdgprc0  34765  fullfunfv  34919  linedegen  35115  bj-inftyexpitaudisj  36086  bj-inftyexpidisj  36091  bj-fvimacnv0  36167  dibvalrel  40034  dicvalrelN  40056  dihvalrel  40150  itgocn  41906  fpwfvss  42163  r1rankcld  42990  grur1cld  42991  uz0  44122  climfveq  44385  climfveqf  44396  afv2ndeffv0  45968  fvmptrabdm  46001  fvconstr  47522  fvconstrn0  47523  fvconstr2  47524  fvconst0ci  47525  fvconstdomi  47526  ipolub00  47618