Theorem ndmfv 6948

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 2605	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5892	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 249	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 153	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6903	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 36	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6908	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 26	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 184	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∃!weu 2596  Vcvv 3454  ∅c0 4281   class class class wbr 5108  dom cdm 5658  ‘cfv 6566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5266  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-dm 5668  df-iota 6520  df-fv 6574

This theorem is used by:  ndmfvrcl  6949  elfvdm  6950  nfvres  6954  fvfundmfvn0  6956  0fv  6957  funfv  7003  fvun1  7007  fvco4i  7018  fvmpti  7023  mptrcl  7034  fvmptss  7037  fvmptex  7039  fvmptnf  7047  fvmptss2  7051  elfvmptrab1  7053  fvopab4ndm  7055  f0cli  7130  fvtp0  7237  funiunfv  7283  funeldmb  7400  ovprc  7489  oprssdm  7634  nssdmovg  7635  ndmovg  7636  1st2val  8063  2nd2val  8064  brovpreldm  8135  soseq  8213  smofvon2  8402  rdgsucmptnf  8475  frsucmptn  8485  brwitnlem  8553  undifixp  9000  r1tr  9820  rankvaln  9844  r1wf  9878  cardidm  10077  carden2a  10084  carden2b  10085  carddomi2  10088  sdomsdomcardi  10089  pm54.43lem  10120  alephcard  10188  alephnbtwn  10189  alephgeom  10200  cfub  10365  cardcf  10368  cflecard  10369  cfle  10370  cflim2  10380  cfidm  10392  itunisuc  10536  itunitc1  10537  ituniiun  10539  alephadd  10701  alephreg  10706  pwcfsdom  10707  cfpwsdom  10708  adderpq  11080  mulerpq  11081  uzssz  13026  ltweuz  14144  wrdsymb0  14735  lsw0  14751  swrd00  14834  swrd0  14850  pfx00  14866  pfx0  14867  sumz  15932  sumss  15934  sumnul  15970  prod1  16155  prodss  16158  divsfval  17769  cidpropd  17934  lubval  18578  glbval  18591  joinval  18599  meetval  18613  gsumpropd2lem  18918  mulgfval  19329  mpfrcl  22449  iscnp2  23612  setsmstopn  24852  tngtopn  25024  dvbsss  26277  perfdvf  26278  dchrrcl  27624  nofv  28071  ltsres  28076  noseponlem  28078  noextenddif  28082  noextendlt  28083  noextendgt  28084  nolesgn2ores  28086  nogesgn1ores  28088  fvnobday  28092  nosepdmlem  28097  nosepssdm  28100  nosupbnd1lem3  28124  nosupbnd1lem5  28126  nosupbnd2lem1  28129  noinfbnd1lem3  28139  noinfbnd1lem5  28141  noinfbnd2lem1  28144  newval  28278  leftval  28292  rightval  28293  lltr  28305  madess  28309  oldssmade  28310  oldss  28313  lrold  28340  structiedg0val  29657  snstriedgval  29673  rgrx0nd  30232  vsfval  31292  dmadjrnb  32565  hmdmadj  32599  acwer1prclem  35892  j0ltaleph  36049  jltaleph  36067  rdgprc0  36770  fullfunfv  36926  linedegen  37123  bj-inftyexpitaudisj  38394  bj-inftyexpidisj  38399  bj-fvimacnv0  38475  dibvalrel  42486  dicvalrelN  42508  dihvalrel  42602  itgocn  44431  fpwfvss  44674  r1rankcld  45490  grur1cld  45491  uz0  46695  climfveq  46952  climfveqf  46963  afv2ndeffv0  48603  fvmptrabdm  48636  ovconstbrd  50304  ovconstbrn0d  50305  elovconstbrd  50306  fvconst0ci  50336  fvconstdomi  50337  ipolub00  50438  oppfrcl  50575  initopropdlemlem  50692  initopropd  50696  termopropd  50697  zeroopropd  50698  fucofvalne  50778