Theorem ndmfv 6849

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541  ∃wex 1780   ∈ wcel 2110  ∃!weu 2562  Vcvv 3434  ∅c0 4281   class class class wbr 5089  dom cdm 5614  ‘cfv 6477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-dm 5624  df-iota 6433  df-fv 6485

This theorem is referenced by:  ndmfvrcl  6850  elfvdm  6851  nfvres  6855  fvfundmfvn0  6857  0fv  6858  funfv  6904  fvun1  6908  fvco4i  6918  fvmpti  6923  mptrcl  6933  fvmptss  6936  fvmptex  6938  fvmptnf  6946  fvmptss2  6950  elfvmptrab1  6952  fvopab4ndm  6954  f0cli  7026  funiunfv  7177  funeldmb  7288  ovprc  7379  oprssdm  7522  nssdmovg  7523  ndmovg  7524  1st2val  7944  2nd2val  7945  brovpreldm  8014  soseq  8084  smofvon2  8271  rdgsucmptnf  8343  frsucmptn  8353  brwitnlem  8417  undifixp  8853  r1tr  9661  rankvaln  9684  cardidm  9844  carden2a  9851  carden2b  9852  carddomi2  9855  sdomsdomcardi  9856  pm54.43lem  9885  alephcard  9953  alephnbtwn  9954  alephgeom  9965  cfub  10132  cardcf  10135  cflecard  10136  cfle  10137  cflim2  10146  cfidm  10158  itunisuc  10302  itunitc1  10303  ituniiun  10305  alephadd  10460  alephreg  10465  pwcfsdom  10466  cfpwsdom  10467  adderpq  10839  mulerpq  10840  uzssz  12745  ltweuz  13860  wrdsymb0  14448  lsw0  14464  swrd00  14544  swrd0  14558  pfx00  14574  pfx0  14575  sumz  15621  sumss  15623  sumnul  15659  prod1  15843  prodss  15846  divsfval  17443  cidpropd  17608  lubval  18252  glbval  18265  joinval  18273  meetval  18287  gsumpropd2lem  18579  mulgfval  18974  mpfrcl  22013  iscnp2  23147  setsmstopn  24386  tngtopn  24558  dvbsss  25823  perfdvf  25824  dchrrcl  27171  nofv  27589  sltres  27594  noseponlem  27596  noextenddif  27600  noextendlt  27601  noextendgt  27602  nolesgn2ores  27604  nogesgn1ores  27606  fvnobday  27610  nosepdmlem  27615  nosepssdm  27618  nosupbnd1lem3  27642  nosupbnd1lem5  27644  nosupbnd2lem1  27647  noinfbnd1lem3  27657  noinfbnd1lem5  27659  noinfbnd2lem1  27662  newval  27789  leftval  27797  rightval  27798  lltropt  27810  madess  27814  oldssmade  27815  oldss  27816  lrold  27835  structiedg0val  28993  snstriedgval  29009  rgrx0nd  29566  vsfval  30603  dmadjrnb  31876  hmdmadj  31910  rdgprc0  35806  fullfunfv  35960  linedegen  36156  bj-inftyexpitaudisj  37218  bj-inftyexpidisj  37223  bj-fvimacnv0  37299  dibvalrel  41181  dicvalrelN  41203  dihvalrel  41297  itgocn  43176  fpwfvss  43424  r1rankcld  44243  grur1cld  44244  uz0  45429  climfveq  45686  climfveqf  45697  afv2ndeffv0  47270  fvmptrabdm  47303  fvconstr  48872  fvconstrn0  48873  fvconstr2  48874  fvconst0ci  48901  fvconstdomi  48902  ipolub00  49003  oppfrcl  49139  initopropdlemlem  49250  initopropd  49254  termopropd  49255  zeroopropd  49256  fucofvalne  49336