Theorem ndmfv 6928

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534  ∃wex 1774   ∈ wcel 2099  ∃!weu 2557  Vcvv 3462  ∅c0 4322   class class class wbr 5145  dom cdm 5674  ‘cfv 6546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-nul 5303  ax-pr 5425

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-dm 5684  df-iota 6498  df-fv 6554

This theorem is referenced by:  ndmfvrcl  6929  elfvdm  6930  nfvres  6934  fvfundmfvn0  6936  0fv  6937  funfv  6981  fvun1  6985  fvco4i  6995  fvmpti  7000  mptrcl  7010  fvmptss  7013  fvmptex  7015  fvmptnf  7023  fvmptss2  7027  elfvmptrab1  7029  fvopab4ndm  7031  f0cli  7104  funiunfv  7255  funeldmb  7363  ovprc  7454  oprssdm  7599  nssdmovg  7600  ndmovg  7601  1st2val  8023  2nd2val  8024  brovpreldm  8095  soseq  8165  smofvon2  8378  rdgsucmptnf  8451  frsucmptn  8461  brwitnlem  8529  undifixp  8955  r1tr  9812  rankvaln  9835  cardidm  9995  carden2a  10002  carden2b  10003  carddomi2  10006  sdomsdomcardi  10007  pm54.43lem  10036  alephcard  10106  alephnbtwn  10107  alephgeom  10118  cfub  10283  cardcf  10286  cflecard  10287  cfle  10288  cflim2  10297  cfidm  10309  itunisuc  10453  itunitc1  10454  ituniiun  10456  alephadd  10611  alephreg  10616  pwcfsdom  10617  cfpwsdom  10618  adderpq  10990  mulerpq  10991  uzssz  12889  ltweuz  13975  wrdsymb0  14552  lsw0  14568  swrd00  14647  swrd0  14661  pfx00  14677  pfx0  14678  sumz  15721  sumss  15723  sumnul  15759  prod1  15941  prodss  15944  divsfval  17557  cidpropd  17718  lubval  18376  glbval  18389  joinval  18397  meetval  18411  gsumpropd2lem  18667  mulgfval  19059  mpfrcl  22096  iscnp2  23231  setsmstopn  24474  tngtopn  24655  dvbsss  25919  perfdvf  25920  dchrrcl  27266  nofv  27684  sltres  27689  noseponlem  27691  noextenddif  27695  noextendlt  27696  noextendgt  27697  nolesgn2ores  27699  nogesgn1ores  27701  fvnobday  27705  nosepdmlem  27710  nosepssdm  27713  nosupbnd1lem3  27737  nosupbnd1lem5  27739  nosupbnd2lem1  27742  noinfbnd1lem3  27752  noinfbnd1lem5  27754  noinfbnd2lem1  27757  newval  27876  leftval  27884  rightval  27885  lltropt  27893  madess  27897  oldssmade  27898  lrold  27917  structiedg0val  28955  snstriedgval  28971  rgrx0nd  29528  vsfval  30563  dmadjrnb  31836  hmdmadj  31870  rdgprc0  35630  fullfunfv  35784  linedegen  35980  bj-inftyexpitaudisj  36925  bj-inftyexpidisj  36930  bj-fvimacnv0  37006  dibvalrel  40875  dicvalrelN  40897  dihvalrel  40991  itgocn  42862  fpwfvss  43116  r1rankcld  43942  grur1cld  43943  uz0  45063  climfveq  45326  climfveqf  45337  afv2ndeffv0  46909  fvmptrabdm  46942  fvconstr  48259  fvconstrn0  48260  fvconstr2  48261  fvconst0ci  48262  fvconstdomi  48263  ipolub00  48355