Theorem ndmfv 6476

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 2596	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5564	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	syl5ibr 238	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 150	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6436	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6439	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 25	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 177	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1601  ∃wex 1823   ∈ wcel 2106  ∃!weu 2585  Vcvv 3397  ∅c0 4140   class class class wbr 4886  dom cdm 5355  ‘cfv 6135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-nul 5025  ax-pow 5077

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-dm 5365  df-iota 6099  df-fv 6143

This theorem is referenced by:  ndmfvrcl  6477  elfvdm  6478  elfvdmOLD  6479  nfvres  6483  fvfundmfvn0  6485  0fv  6486  funfv  6525  fvun1  6529  fvco4i  6536  fvmpti  6541  mptrcl  6550  fvmptss  6553  fvmptex  6555  fvmptnf  6563  fvmptss2  6566  elfvmptrab1  6567  fvopab4ndm  6569  f0cli  6634  funiunfv  6778  ovprc  6959  oprssdm  7092  nssdmovg  7093  ndmovg  7094  1st2val  7473  2nd2val  7474  brovpreldm  7535  smofvon2  7736  rdgsucmptnf  7808  frsucmptn  7817  brwitnlem  7871  undifixp  8230  r1tr  8936  rankvaln  8959  cardidm  9118  carden2a  9125  carden2b  9126  carddomi2  9129  sdomsdomcardi  9130  pm54.43lem  9158  alephcard  9226  alephnbtwn  9227  alephgeom  9238  cfub  9406  cardcf  9409  cflecard  9410  cfle  9411  cflim2  9420  cfidm  9432  itunisuc  9576  itunitc1  9577  ituniiun  9579  alephadd  9734  alephreg  9739  pwcfsdom  9740  cfpwsdom  9741  adderpq  10113  mulerpq  10114  uzssz  12012  ltweuz  13079  wrdsymb0  13639  lsw0  13655  swrd00  13734  swrd0  13753  pfx00  13783  pfx0  13784  sumz  14860  sumss  14862  sumnul  14896  prod1  15077  prodss  15080  divsfval  16593  cidpropd  16755  arwval  17078  coafval  17099  lubval  17370  glbval  17383  joinval  17391  meetval  17405  gsumpropd2lem  17659  mpfrcl  19914  iscnp2  21451  setsmstopn  22691  tngtopn  22862  pcofval  23217  dvbsss  24103  perfdvf  24104  dchrrcl  25417  eleenn  26245  structiedg0val  26370  snstriedgval  26386  rgrx0nd  26942  vsfval  28060  dmadjrnb  29337  hmdmadj  29371  funeldmb  32254  rdgprc0  32287  soseq  32343  nofv  32399  sltres  32404  noseponlem  32406  noextenddif  32410  noextendlt  32411  noextendgt  32412  nolesgn2ores  32414  fvnobday  32418  nosepdmlem  32422  nosepssdm  32425  nosupbnd1lem3  32445  nosupbnd1lem5  32447  nosupbnd2lem1  32450  fullfunfv  32643  linedegen  32839  bj-inftyexpitaudisj  33682  bj-inftyexpidisj  33687  dibvalrel  37301  dicvalrelN  37323  dihvalrel  37417  itgocn  38675  uz0  40527  climfveq  40791  climfveqf  40802  afv2ndeffv0  42283  fvmptrabdm  42316  setrec2lem1  43527