Theorem ndmfv 6910

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 2602	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5882	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 249	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 153	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6865	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 36	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6870	. . 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 2145  ∃!weu 2593  Vcvv 3450  ∅c0 4279   class class class wbr 5103  dom cdm 5655  ‘cfv 6533

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5263  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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-dm 5665  df-iota 6489  df-fv 6541

This theorem is used by:  ndmfvrcl  6911  elfvdm  6912  nfvres  6916  fvfundmfvn0  6918  0fv  6919  funfv  6965  fvun1  6969  fvco4i  6980  fvmpti  6985  mptrcl  6996  fvmptss  6999  fvmptex  7001  fvmptnf  7009  fvmptss2  7013  elfvmptrab1  7015  fvopab4ndm  7017  f0cli  7091  fvtp0  7199  funiunfv  7245  funeldmb  7362  ovprc  7451  oprssdm  7595  nssdmovg  7596  ndmovg  7597  1st2val  8014  2nd2val  8015  brovpreldm  8086  soseq  8157  smofvon2  8345  rdgsucmptnf  8418  frsucmptn  8428  brwitnlem  8494  undifixp  8941  r1tr  9758  rankvaln  9781  cardidm  9964  carden2a  9971  carden2b  9972  carddomi2  9975  sdomsdomcardi  9976  pm54.43lem  10005  alephcard  10073  alephnbtwn  10074  alephgeom  10085  cfub  10250  cardcf  10253  cflecard  10254  cfle  10255  cflim2  10265  cfidm  10277  itunisuc  10421  itunitc1  10422  ituniiun  10424  alephadd  10586  alephreg  10591  pwcfsdom  10592  cfpwsdom  10593  adderpq  10965  mulerpq  10966  uzssz  12908  ltweuz  14025  wrdsymb0  14614  lsw0  14630  swrd00  14712  swrd0  14728  pfx00  14744  pfx0  14745  sumz  15808  sumss  15810  sumnul  15846  prod1  16031  prodss  16034  divsfval  17633  cidpropd  17798  lubval  18442  glbval  18455  joinval  18463  meetval  18477  gsumpropd2lem  18781  mulgfval  19192  mpfrcl  22301  iscnp2  23464  setsmstopn  24704  tngtopn  24876  dvbsss  26129  perfdvf  26130  dchrrcl  27476  nofv  27893  ltsres  27898  noseponlem  27900  noextenddif  27904  noextendlt  27905  noextendgt  27906  nolesgn2ores  27908  nogesgn1ores  27910  fvnobday  27914  nosepdmlem  27919  nosepssdm  27922  nosupbnd1lem3  27946  nosupbnd1lem5  27948  nosupbnd2lem1  27951  noinfbnd1lem3  27961  noinfbnd1lem5  27963  noinfbnd2lem1  27966  newval  28100  leftval  28114  rightval  28115  lltr  28127  madess  28131  oldssmade  28132  oldss  28135  lrold  28162  structiedg0val  29479  snstriedgval  29495  rgrx0nd  30054  vsfval  31114  dmadjrnb  32387  hmdmadj  32421  r1wf  35603  rdgprc0  36370  fullfunfv  36526  linedegen  36723  bj-inftyexpitaudisj  37957  bj-inftyexpidisj  37962  bj-fvimacnv0  38038  dibvalrel  42036  dicvalrelN  42058  dihvalrel  42152  itgocn  44005  fpwfvss  44252  r1rankcld  45069  grur1cld  45070  uz0  46240  climfveq  46497  climfveqf  46508  afv2ndeffv0  48148  fvmptrabdm  48181  fvconstr  49790  fvconstrn0  49791  fvconstr2  49792  fvconst0ci  49817  fvconstdomi  49818  ipolub00  49919  oppfrcl  50054  initopropdlemlem  50165  initopropd  50169  termopropd  50170  zeroopropd  50171  fucofvalne  50251