Theorem ndmfv 6955

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 2580	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5923	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 246	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6908	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6912	. . 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 1777   ∈ wcel 2108  ∃!weu 2571  Vcvv 3488  ∅c0 4352   class class class wbr 5166  dom cdm 5700  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-dm 5710  df-iota 6525  df-fv 6581

This theorem is referenced by:  ndmfvrcl  6956  elfvdm  6957  nfvres  6961  fvfundmfvn0  6963  0fv  6964  funfv  7009  fvun1  7013  fvco4i  7023  fvmpti  7028  mptrcl  7038  fvmptss  7041  fvmptex  7043  fvmptnf  7051  fvmptss2  7055  elfvmptrab1  7057  fvopab4ndm  7059  f0cli  7132  funiunfv  7285  funeldmb  7395  ovprc  7486  oprssdm  7631  nssdmovg  7632  ndmovg  7633  1st2val  8058  2nd2val  8059  brovpreldm  8130  soseq  8200  smofvon2  8412  rdgsucmptnf  8485  frsucmptn  8495  brwitnlem  8563  undifixp  8992  r1tr  9845  rankvaln  9868  cardidm  10028  carden2a  10035  carden2b  10036  carddomi2  10039  sdomsdomcardi  10040  pm54.43lem  10069  alephcard  10139  alephnbtwn  10140  alephgeom  10151  cfub  10318  cardcf  10321  cflecard  10322  cfle  10323  cflim2  10332  cfidm  10344  itunisuc  10488  itunitc1  10489  ituniiun  10491  alephadd  10646  alephreg  10651  pwcfsdom  10652  cfpwsdom  10653  adderpq  11025  mulerpq  11026  uzssz  12924  ltweuz  14012  wrdsymb0  14597  lsw0  14613  swrd00  14692  swrd0  14706  pfx00  14722  pfx0  14723  sumz  15770  sumss  15772  sumnul  15808  prod1  15992  prodss  15995  divsfval  17607  cidpropd  17768  lubval  18426  glbval  18439  joinval  18447  meetval  18461  gsumpropd2lem  18717  mulgfval  19109  mpfrcl  22132  iscnp2  23268  setsmstopn  24511  tngtopn  24692  dvbsss  25957  perfdvf  25958  dchrrcl  27302  nofv  27720  sltres  27725  noseponlem  27727  noextenddif  27731  noextendlt  27732  noextendgt  27733  nolesgn2ores  27735  nogesgn1ores  27737  fvnobday  27741  nosepdmlem  27746  nosepssdm  27749  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd2lem1  27778  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd2lem1  27793  newval  27912  leftval  27920  rightval  27921  lltropt  27929  madess  27933  oldssmade  27934  lrold  27953  structiedg0val  29057  snstriedgval  29073  rgrx0nd  29630  vsfval  30665  dmadjrnb  31938  hmdmadj  31972  rdgprc0  35757  fullfunfv  35911  linedegen  36107  bj-inftyexpitaudisj  37171  bj-inftyexpidisj  37176  bj-fvimacnv0  37252  dibvalrel  41120  dicvalrelN  41142  dihvalrel  41236  itgocn  43121  fpwfvss  43374  r1rankcld  44200  grur1cld  44201  uz0  45327  climfveq  45590  climfveqf  45601  afv2ndeffv0  47175  fvmptrabdm  47208  fvconstr  48569  fvconstrn0  48570  fvconstr2  48571  fvconst0ci  48572  fvconstdomi  48573  ipolub00  48665