Theorem ndmfv 6924

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542  ∃wex 1782   ∈ wcel 2107  ∃!weu 2563  Vcvv 3475  ∅c0 4322   class class class wbr 5148  dom cdm 5676  ‘cfv 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-dm 5686  df-iota 6493  df-fv 6549

This theorem is referenced by:  ndmfvrcl  6925  elfvdm  6926  nfvres  6930  fvfundmfvn0  6932  0fv  6933  funfv  6976  fvun1  6980  fvco4i  6990  fvmpti  6995  mptrcl  7005  fvmptss  7008  fvmptex  7010  fvmptnf  7018  fvmptss2  7021  elfvmptrab1  7023  fvopab4ndm  7025  f0cli  7097  funiunfv  7244  funeldmb  7353  ovprc  7444  oprssdm  7585  nssdmovg  7586  ndmovg  7587  1st2val  8000  2nd2val  8001  brovpreldm  8072  soseq  8142  smofvon2  8353  rdgsucmptnf  8426  frsucmptn  8436  brwitnlem  8504  undifixp  8925  r1tr  9768  rankvaln  9791  cardidm  9951  carden2a  9958  carden2b  9959  carddomi2  9962  sdomsdomcardi  9963  pm54.43lem  9992  alephcard  10062  alephnbtwn  10063  alephgeom  10074  cfub  10241  cardcf  10244  cflecard  10245  cfle  10246  cflim2  10255  cfidm  10267  itunisuc  10411  itunitc1  10412  ituniiun  10414  alephadd  10569  alephreg  10574  pwcfsdom  10575  cfpwsdom  10576  adderpq  10948  mulerpq  10949  uzssz  12840  ltweuz  13923  wrdsymb0  14496  lsw0  14512  swrd00  14591  swrd0  14605  pfx00  14621  pfx0  14622  sumz  15665  sumss  15667  sumnul  15703  prod1  15885  prodss  15888  divsfval  17490  cidpropd  17651  lubval  18306  glbval  18319  joinval  18327  meetval  18341  gsumpropd2lem  18595  mulgfval  18947  mpfrcl  21640  iscnp2  22735  setsmstopn  23978  tngtopn  24159  dvbsss  25411  perfdvf  25412  dchrrcl  26733  nofv  27150  sltres  27155  noseponlem  27157  noextenddif  27161  noextendlt  27162  noextendgt  27163  nolesgn2ores  27165  nogesgn1ores  27167  fvnobday  27171  nosepdmlem  27176  nosepssdm  27179  nosupbnd1lem3  27203  nosupbnd1lem5  27205  nosupbnd2lem1  27208  noinfbnd1lem3  27218  noinfbnd1lem5  27220  noinfbnd2lem1  27223  newval  27340  leftval  27348  rightval  27349  lltropt  27357  madess  27361  oldssmade  27362  lrold  27381  structiedg0val  28272  snstriedgval  28288  rgrx0nd  28841  vsfval  29874  dmadjrnb  31147  hmdmadj  31181  rdgprc0  34754  fullfunfv  34908  linedegen  35104  bj-inftyexpitaudisj  36075  bj-inftyexpidisj  36080  bj-fvimacnv0  36156  dibvalrel  40023  dicvalrelN  40045  dihvalrel  40139  itgocn  41892  fpwfvss  42149  r1rankcld  42976  grur1cld  42977  uz0  44109  climfveq  44372  climfveqf  44383  afv2ndeffv0  45955  fvmptrabdm  45988  fvconstr  47476  fvconstrn0  47477  fvconstr2  47478  fvconst0ci  47479  fvconstdomi  47480  ipolub00  47572