Theorem ndmfv 6893

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 2570	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5862	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 246	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6846	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6850	. . 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 2561  Vcvv 3447  ∅c0 4296   class class class wbr 5107  dom cdm 5638  ‘cfv 6511

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 2701  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-dm 5648  df-iota 6464  df-fv 6519

This theorem is referenced by:  ndmfvrcl  6894  elfvdm  6895  nfvres  6899  fvfundmfvn0  6901  0fv  6902  funfv  6948  fvun1  6952  fvco4i  6962  fvmpti  6967  mptrcl  6977  fvmptss  6980  fvmptex  6982  fvmptnf  6990  fvmptss2  6994  elfvmptrab1  6996  fvopab4ndm  6998  f0cli  7070  funiunfv  7222  funeldmb  7334  ovprc  7425  oprssdm  7570  nssdmovg  7571  ndmovg  7572  1st2val  7996  2nd2val  7997  brovpreldm  8068  soseq  8138  smofvon2  8325  rdgsucmptnf  8397  frsucmptn  8407  brwitnlem  8471  undifixp  8907  r1tr  9729  rankvaln  9752  cardidm  9912  carden2a  9919  carden2b  9920  carddomi2  9923  sdomsdomcardi  9924  pm54.43lem  9953  alephcard  10023  alephnbtwn  10024  alephgeom  10035  cfub  10202  cardcf  10205  cflecard  10206  cfle  10207  cflim2  10216  cfidm  10228  itunisuc  10372  itunitc1  10373  ituniiun  10375  alephadd  10530  alephreg  10535  pwcfsdom  10536  cfpwsdom  10537  adderpq  10909  mulerpq  10910  uzssz  12814  ltweuz  13926  wrdsymb0  14514  lsw0  14530  swrd00  14609  swrd0  14623  pfx00  14639  pfx0  14640  sumz  15688  sumss  15690  sumnul  15726  prod1  15910  prodss  15913  divsfval  17510  cidpropd  17671  lubval  18315  glbval  18328  joinval  18336  meetval  18350  gsumpropd2lem  18606  mulgfval  19001  mpfrcl  21992  iscnp2  23126  setsmstopn  24366  tngtopn  24538  dvbsss  25803  perfdvf  25804  dchrrcl  27151  nofv  27569  sltres  27574  noseponlem  27576  noextenddif  27580  noextendlt  27581  noextendgt  27582  nolesgn2ores  27584  nogesgn1ores  27586  fvnobday  27590  nosepdmlem  27595  nosepssdm  27598  nosupbnd1lem3  27622  nosupbnd1lem5  27624  nosupbnd2lem1  27627  noinfbnd1lem3  27637  noinfbnd1lem5  27639  noinfbnd2lem1  27642  newval  27763  leftval  27771  rightval  27772  lltropt  27784  madess  27788  oldssmade  27789  lrold  27808  structiedg0val  28949  snstriedgval  28965  rgrx0nd  29522  vsfval  30562  dmadjrnb  31835  hmdmadj  31869  rdgprc0  35781  fullfunfv  35935  linedegen  36131  bj-inftyexpitaudisj  37193  bj-inftyexpidisj  37198  bj-fvimacnv0  37274  dibvalrel  41157  dicvalrelN  41179  dihvalrel  41273  itgocn  43153  fpwfvss  43401  r1rankcld  44220  grur1cld  44221  uz0  45408  climfveq  45667  climfveqf  45678  afv2ndeffv0  47261  fvmptrabdm  47294  fvconstr  48850  fvconstrn0  48851  fvconstr2  48852  fvconst0ci  48879  fvconstdomi  48880  ipolub00  48981  oppfrcl  49117  initopropdlemlem  49228  initopropd  49232  termopropd  49233  zeroopropd  49234  fucofvalne  49314