Theorem ndmfv 6916

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃!weu 2568  Vcvv 3464  ∅c0 4313   class class class wbr 5124  dom cdm 5659  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-dm 5669  df-iota 6489  df-fv 6544

This theorem is referenced by:  ndmfvrcl  6917  elfvdm  6918  nfvres  6922  fvfundmfvn0  6924  0fv  6925  funfv  6971  fvun1  6975  fvco4i  6985  fvmpti  6990  mptrcl  7000  fvmptss  7003  fvmptex  7005  fvmptnf  7013  fvmptss2  7017  elfvmptrab1  7019  fvopab4ndm  7021  f0cli  7093  funiunfv  7245  funeldmb  7357  ovprc  7448  oprssdm  7593  nssdmovg  7594  ndmovg  7595  1st2val  8021  2nd2val  8022  brovpreldm  8093  soseq  8163  smofvon2  8375  rdgsucmptnf  8448  frsucmptn  8458  brwitnlem  8524  undifixp  8953  r1tr  9795  rankvaln  9818  cardidm  9978  carden2a  9985  carden2b  9986  carddomi2  9989  sdomsdomcardi  9990  pm54.43lem  10019  alephcard  10089  alephnbtwn  10090  alephgeom  10101  cfub  10268  cardcf  10271  cflecard  10272  cfle  10273  cflim2  10282  cfidm  10294  itunisuc  10438  itunitc1  10439  ituniiun  10441  alephadd  10596  alephreg  10601  pwcfsdom  10602  cfpwsdom  10603  adderpq  10975  mulerpq  10976  uzssz  12878  ltweuz  13984  wrdsymb0  14572  lsw0  14588  swrd00  14667  swrd0  14681  pfx00  14697  pfx0  14698  sumz  15743  sumss  15745  sumnul  15781  prod1  15965  prodss  15968  divsfval  17566  cidpropd  17727  lubval  18371  glbval  18384  joinval  18392  meetval  18406  gsumpropd2lem  18662  mulgfval  19057  mpfrcl  22048  iscnp2  23182  setsmstopn  24422  tngtopn  24594  dvbsss  25860  perfdvf  25861  dchrrcl  27208  nofv  27626  sltres  27631  noseponlem  27633  noextenddif  27637  noextendlt  27638  noextendgt  27639  nolesgn2ores  27641  nogesgn1ores  27643  fvnobday  27647  nosepdmlem  27652  nosepssdm  27655  nosupbnd1lem3  27679  nosupbnd1lem5  27681  nosupbnd2lem1  27684  noinfbnd1lem3  27694  noinfbnd1lem5  27696  noinfbnd2lem1  27699  newval  27820  leftval  27828  rightval  27829  lltropt  27841  madess  27845  oldssmade  27846  lrold  27865  structiedg0val  29006  snstriedgval  29022  rgrx0nd  29579  vsfval  30619  dmadjrnb  31892  hmdmadj  31926  rdgprc0  35816  fullfunfv  35970  linedegen  36166  bj-inftyexpitaudisj  37228  bj-inftyexpidisj  37233  bj-fvimacnv0  37309  dibvalrel  41187  dicvalrelN  41209  dihvalrel  41303  itgocn  43163  fpwfvss  43411  r1rankcld  44230  grur1cld  44231  uz0  45419  climfveq  45678  climfveqf  45689  afv2ndeffv0  47269  fvmptrabdm  47302  fvconstr  48818  fvconstrn0  48819  fvconstr2  48820  fvconst0ci  48846  fvconstdomi  48847  ipolub00  48947  oppfrcl  49056  initopropdlemlem  49136  initopropd  49140  termopropd  49141  zeroopropd  49142  fucofvalne  49216