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 2572	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5833	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 246	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6804	. . 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 2111  ∃!weu 2563  Vcvv 3436  ∅c0 4278   class class class wbr 5086  dom cdm 5611  ‘cfv 6476

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 2113  ax-9 2121  ax-ext 2703  ax-nul 5239  ax-pr 5365

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-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-dm 5621  df-iota 6432  df-fv 6484

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  9664  rankvaln  9687  cardidm  9847  carden2a  9854  carden2b  9855  carddomi2  9858  sdomsdomcardi  9859  pm54.43lem  9888  alephcard  9956  alephnbtwn  9957  alephgeom  9968  cfub  10135  cardcf  10138  cflecard  10139  cfle  10140  cflim2  10149  cfidm  10161  itunisuc  10305  itunitc1  10306  ituniiun  10308  alephadd  10463  alephreg  10468  pwcfsdom  10469  cfpwsdom  10470  adderpq  10842  mulerpq  10843  uzssz  12748  ltweuz  13863  wrdsymb0  14451  lsw0  14467  swrd00  14547  swrd0  14561  pfx00  14577  pfx0  14578  sumz  15624  sumss  15626  sumnul  15662  prod1  15846  prodss  15849  divsfval  17446  cidpropd  17611  lubval  18255  glbval  18268  joinval  18276  meetval  18290  gsumpropd2lem  18582  mulgfval  18977  mpfrcl  22015  iscnp2  23149  setsmstopn  24388  tngtopn  24560  dvbsss  25825  perfdvf  25826  dchrrcl  27173  nofv  27591  sltres  27596  noseponlem  27598  noextenddif  27602  noextendlt  27603  noextendgt  27604  nolesgn2ores  27606  nogesgn1ores  27608  fvnobday  27612  nosepdmlem  27617  nosepssdm  27620  nosupbnd1lem3  27644  nosupbnd1lem5  27646  nosupbnd2lem1  27649  noinfbnd1lem3  27659  noinfbnd1lem5  27661  noinfbnd2lem1  27664  newval  27791  leftval  27799  rightval  27800  lltropt  27812  madess  27816  oldssmade  27817  oldss  27818  lrold  27837  structiedg0val  28995  snstriedgval  29011  rgrx0nd  29568  vsfval  30605  dmadjrnb  31878  hmdmadj  31912  r1wf  35099  rdgprc0  35827  fullfunfv  35981  linedegen  36177  bj-inftyexpitaudisj  37239  bj-inftyexpidisj  37244  bj-fvimacnv0  37320  dibvalrel  41202  dicvalrelN  41224  dihvalrel  41318  itgocn  43197  fpwfvss  43445  r1rankcld  44264  grur1cld  44265  uz0  45450  climfveq  45707  climfveqf  45718  afv2ndeffv0  47291  fvmptrabdm  47324  fvconstr  48893  fvconstrn0  48894  fvconstr2  48895  fvconst0ci  48922  fvconstdomi  48923  ipolub00  49024  oppfrcl  49160  initopropdlemlem  49271  initopropd  49275  termopropd  49276  zeroopropd  49277  fucofvalne  49357