Theorem ndmfv 6894

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559  ∃wex 1798   ∈ wcel 2141  ∃!weu 2594  Vcvv 3453  ∅c0 4283   class class class wbr 5097  dom cdm 5643  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-dm 5653  df-iota 6472  df-fv 6524

This theorem is referenced by:  ndmfvrcl  6895  elfvdm  6896  nfvres  6900  fvfundmfvn0  6902  0fv  6903  funfv  6949  fvun1  6953  fvco4i  6964  fvmpti  6969  mptrcl  6980  fvmptss  6983  fvmptex  6985  fvmptnf  6993  fvmptss2  6997  elfvmptrab1  6999  fvopab4ndm  7001  f0cli  7074  funiunfv  7227  funeldmb  7338  ovprc  7429  oprssdm  7572  nssdmovg  7573  ndmovg  7574  1st2val  7993  2nd2val  7994  brovpreldm  8062  soseq  8133  smofvon2  8321  rdgsucmptnf  8394  frsucmptn  8404  brwitnlem  8470  undifixp  8910  r1tr  9728  rankvaln  9751  cardidm  9911  carden2a  9918  carden2b  9919  carddomi2  9922  sdomsdomcardi  9923  pm54.43lem  9952  alephcard  10020  alephnbtwn  10021  alephgeom  10032  cfub  10199  cardcf  10202  cflecard  10203  cfle  10204  cflim2  10214  cfidm  10226  itunisuc  10370  itunitc1  10371  ituniiun  10373  alephadd  10529  alephreg  10534  pwcfsdom  10535  cfpwsdom  10536  adderpq  10908  mulerpq  10909  uzssz  12854  ltweuz  13968  wrdsymb0  14556  lsw0  14572  swrd00  14652  swrd0  14666  pfx00  14682  pfx0  14683  sumz  15740  sumss  15742  sumnul  15778  prod1  15965  prodss  15968  divsfval  17568  cidpropd  17733  lubval  18377  glbval  18390  joinval  18398  meetval  18412  gsumpropd2lem  18704  mulgfval  19102  mpfrcl  22126  iscnp2  23287  setsmstopn  24526  tngtopn  24698  dvbsss  25952  perfdvf  25953  dchrrcl  27292  nofv  27709  ltsres  27714  noseponlem  27716  noextenddif  27720  noextendlt  27721  noextendgt  27722  nolesgn2ores  27724  nogesgn1ores  27726  fvnobday  27730  nosepdmlem  27735  nosepssdm  27738  nosupbnd1lem3  27762  nosupbnd1lem5  27764  nosupbnd2lem1  27767  noinfbnd1lem3  27777  noinfbnd1lem5  27779  noinfbnd2lem1  27782  newval  27916  leftval  27930  rightval  27931  lltr  27943  madess  27947  oldssmade  27948  oldss  27951  lrold  27978  structiedg0val  29180  snstriedgval  29196  rgrx0nd  29752  vsfval  30793  dmadjrnb  32066  hmdmadj  32100  r1wf  35353  rdgprc0  36102  fullfunfv  36258  linedegen  36454  bj-inftyexpitaudisj  37658  bj-inftyexpidisj  37663  bj-fvimacnv0  37739  dibvalrel  41748  dicvalrelN  41770  dihvalrel  41864  itgocn  43702  fpwfvss  43949  r1rankcld  44768  grur1cld  44769  uz0  45947  climfveq  46204  climfveqf  46215  afv2ndeffv0  47815  fvmptrabdm  47848  fvconstr  49444  fvconstrn0  49445  fvconstr2  49446  fvconst0ci  49473  fvconstdomi  49474  ipolub00  49575  oppfrcl  49710  initopropdlemlem  49821  initopropd  49825  termopropd  49826  zeroopropd  49827  fucofvalne  49907