Theorem ndmfv 6875

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 5852	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 246	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6828	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6832	. . 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 3444  ∅c0 4292   class class class wbr 5102  dom cdm 5631  ‘cfv 6499

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 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-dm 5641  df-iota 6452  df-fv 6507

This theorem is referenced by:  ndmfvrcl  6876  elfvdm  6877  nfvres  6881  fvfundmfvn0  6883  0fv  6884  funfv  6930  fvun1  6934  fvco4i  6944  fvmpti  6949  mptrcl  6959  fvmptss  6962  fvmptex  6964  fvmptnf  6972  fvmptss2  6976  elfvmptrab1  6978  fvopab4ndm  6980  f0cli  7052  funiunfv  7204  funeldmb  7316  ovprc  7407  oprssdm  7550  nssdmovg  7551  ndmovg  7552  1st2val  7975  2nd2val  7976  brovpreldm  8045  soseq  8115  smofvon2  8302  rdgsucmptnf  8374  frsucmptn  8384  brwitnlem  8448  undifixp  8884  r1tr  9705  rankvaln  9728  cardidm  9888  carden2a  9895  carden2b  9896  carddomi2  9899  sdomsdomcardi  9900  pm54.43lem  9929  alephcard  9999  alephnbtwn  10000  alephgeom  10011  cfub  10178  cardcf  10181  cflecard  10182  cfle  10183  cflim2  10192  cfidm  10204  itunisuc  10348  itunitc1  10349  ituniiun  10351  alephadd  10506  alephreg  10511  pwcfsdom  10512  cfpwsdom  10513  adderpq  10885  mulerpq  10886  uzssz  12790  ltweuz  13902  wrdsymb0  14490  lsw0  14506  swrd00  14585  swrd0  14599  pfx00  14615  pfx0  14616  sumz  15664  sumss  15666  sumnul  15702  prod1  15886  prodss  15889  divsfval  17486  cidpropd  17647  lubval  18291  glbval  18304  joinval  18312  meetval  18326  gsumpropd2lem  18582  mulgfval  18977  mpfrcl  21968  iscnp2  23102  setsmstopn  24342  tngtopn  24514  dvbsss  25779  perfdvf  25780  dchrrcl  27127  nofv  27545  sltres  27550  noseponlem  27552  noextenddif  27556  noextendlt  27557  noextendgt  27558  nolesgn2ores  27560  nogesgn1ores  27562  fvnobday  27566  nosepdmlem  27571  nosepssdm  27574  nosupbnd1lem3  27598  nosupbnd1lem5  27600  nosupbnd2lem1  27603  noinfbnd1lem3  27613  noinfbnd1lem5  27615  noinfbnd2lem1  27618  newval  27739  leftval  27747  rightval  27748  lltropt  27760  madess  27764  oldssmade  27765  lrold  27784  structiedg0val  28925  snstriedgval  28941  rgrx0nd  29498  vsfval  30535  dmadjrnb  31808  hmdmadj  31842  rdgprc0  35754  fullfunfv  35908  linedegen  36104  bj-inftyexpitaudisj  37166  bj-inftyexpidisj  37171  bj-fvimacnv0  37247  dibvalrel  41130  dicvalrelN  41152  dihvalrel  41246  itgocn  43126  fpwfvss  43374  r1rankcld  44193  grur1cld  44194  uz0  45381  climfveq  45640  climfveqf  45651  afv2ndeffv0  47234  fvmptrabdm  47267  fvconstr  48823  fvconstrn0  48824  fvconstr2  48825  fvconst0ci  48852  fvconstdomi  48853  ipolub00  48954  oppfrcl  49090  initopropdlemlem  49201  initopropd  49205  termopropd  49206  zeroopropd  49207  fucofvalne  49287