Theorem ndmfv 6786

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 2577	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5796	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	syl5ibr 245	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6745	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6748	. . 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 1783   ∈ wcel 2108  ∃!weu 2568  Vcvv 3422  ∅c0 4253   class class class wbr 5070  dom cdm 5580  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-dm 5590  df-iota 6376  df-fv 6426

This theorem is referenced by:  ndmfvrcl  6787  elfvdm  6788  nfvres  6792  fvfundmfvn0  6794  0fv  6795  funfv  6837  fvun1  6841  fvco4i  6851  fvmpti  6856  mptrcl  6866  fvmptss  6869  fvmptex  6871  fvmptnf  6879  fvmptss2  6882  elfvmptrab1  6884  fvopab4ndm  6886  f0cli  6956  funiunfv  7103  ovprc  7293  oprssdm  7431  nssdmovg  7432  ndmovg  7433  1st2val  7832  2nd2val  7833  brovpreldm  7900  smofvon2  8158  rdgsucmptnf  8231  frsucmptn  8240  brwitnlem  8299  undifixp  8680  r1tr  9465  rankvaln  9488  cardidm  9648  carden2a  9655  carden2b  9656  carddomi2  9659  sdomsdomcardi  9660  pm54.43lem  9689  alephcard  9757  alephnbtwn  9758  alephgeom  9769  cfub  9936  cardcf  9939  cflecard  9940  cfle  9941  cflim2  9950  cfidm  9962  itunisuc  10106  itunitc1  10107  ituniiun  10109  alephadd  10264  alephreg  10269  pwcfsdom  10270  cfpwsdom  10271  adderpq  10643  mulerpq  10644  uzssz  12532  ltweuz  13609  wrdsymb0  14180  lsw0  14196  swrd00  14285  swrd0  14299  pfx00  14315  pfx0  14316  sumz  15362  sumss  15364  sumnul  15400  prod1  15582  prodss  15585  divsfval  17175  cidpropd  17336  lubval  17989  glbval  18002  joinval  18010  meetval  18024  gsumpropd2lem  18278  mulgfval  18617  mpfrcl  21205  iscnp2  22298  setsmstopn  23539  tngtopn  23720  dvbsss  24971  perfdvf  24972  dchrrcl  26293  structiedg0val  27295  snstriedgval  27311  rgrx0nd  27864  vsfval  28896  dmadjrnb  30169  hmdmadj  30203  funeldmb  33643  rdgprc0  33675  soseq  33730  nofv  33787  sltres  33792  noseponlem  33794  noextenddif  33798  noextendlt  33799  noextendgt  33800  nolesgn2ores  33802  nogesgn1ores  33804  fvnobday  33808  nosepdmlem  33813  nosepssdm  33816  nosupbnd1lem3  33840  nosupbnd1lem5  33842  nosupbnd2lem1  33845  noinfbnd1lem3  33855  noinfbnd1lem5  33857  noinfbnd2lem1  33860  newval  33966  leftval  33974  rightval  33975  madess  33986  oldssmade  33987  lrold  34004  fullfunfv  34176  linedegen  34372  bj-inftyexpitaudisj  35303  bj-inftyexpidisj  35308  bj-fvimacnv0  35384  dibvalrel  39104  dicvalrelN  39126  dihvalrel  39220  itgocn  40905  r1rankcld  41738  grur1cld  41739  uz0  42842  climfveq  43100  climfveqf  43111  afv2ndeffv0  44639  fvmptrabdm  44672  fvconstr  46071  fvconstrn0  46072  fvconstr2  46073  fvconst0ci  46074  fvconstdomi  46075  ipolub00  46167