Theorem ndmfv 6860

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 2575	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5840	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	syl5ibr 245	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6813	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6817	. . 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 1780   ∈ wcel 2105  ∃!weu 2566  Vcvv 3441  ∅c0 4269   class class class wbr 5092  dom cdm 5620  ‘cfv 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-nul 5250  ax-pr 5372

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-dm 5630  df-iota 6431  df-fv 6487

This theorem is referenced by:  ndmfvrcl  6861  elfvdm  6862  nfvres  6866  fvfundmfvn0  6868  0fv  6869  funfv  6911  fvun1  6915  fvco4i  6925  fvmpti  6930  mptrcl  6940  fvmptss  6943  fvmptex  6945  fvmptnf  6953  fvmptss2  6956  elfvmptrab1  6958  fvopab4ndm  6960  f0cli  7030  funiunfv  7177  funeldmb  7286  ovprc  7375  oprssdm  7515  nssdmovg  7516  ndmovg  7517  1st2val  7927  2nd2val  7928  brovpreldm  7997  soseq  8046  smofvon2  8257  rdgsucmptnf  8330  frsucmptn  8340  brwitnlem  8408  undifixp  8793  r1tr  9633  rankvaln  9656  cardidm  9816  carden2a  9823  carden2b  9824  carddomi2  9827  sdomsdomcardi  9828  pm54.43lem  9857  alephcard  9927  alephnbtwn  9928  alephgeom  9939  cfub  10106  cardcf  10109  cflecard  10110  cfle  10111  cflim2  10120  cfidm  10132  itunisuc  10276  itunitc1  10277  ituniiun  10279  alephadd  10434  alephreg  10439  pwcfsdom  10440  cfpwsdom  10441  adderpq  10813  mulerpq  10814  uzssz  12704  ltweuz  13782  wrdsymb0  14352  lsw0  14368  swrd00  14455  swrd0  14469  pfx00  14485  pfx0  14486  sumz  15533  sumss  15535  sumnul  15571  prod1  15753  prodss  15756  divsfval  17355  cidpropd  17516  lubval  18171  glbval  18184  joinval  18192  meetval  18206  gsumpropd2lem  18460  mulgfval  18798  mpfrcl  21401  iscnp2  22496  setsmstopn  23739  tngtopn  23920  dvbsss  25172  perfdvf  25173  dchrrcl  26494  nofv  26911  sltres  26916  noseponlem  26918  noextenddif  26922  noextendlt  26923  noextendgt  26924  nolesgn2ores  26926  nogesgn1ores  26928  fvnobday  26932  nosepdmlem  26937  nosepssdm  26940  nosupbnd1lem3  26964  nosupbnd1lem5  26966  nosupbnd2lem1  26969  noinfbnd1lem3  26979  noinfbnd1lem5  26981  noinfbnd2lem1  26984  structiedg0val  27681  snstriedgval  27697  rgrx0nd  28250  vsfval  29283  dmadjrnb  30556  hmdmadj  30590  rdgprc0  34052  newval  34135  leftval  34143  rightval  34144  madess  34155  oldssmade  34156  lrold  34173  fullfunfv  34345  linedegen  34541  bj-inftyexpitaudisj  35489  bj-inftyexpidisj  35494  bj-fvimacnv0  35570  dibvalrel  39439  dicvalrelN  39461  dihvalrel  39555  itgocn  41260  fpwfvss  41349  r1rankcld  42178  grur1cld  42179  uz0  43295  climfveq  43554  climfveqf  43565  afv2ndeffv0  45111  fvmptrabdm  45144  fvconstr  46542  fvconstrn0  46543  fvconstr2  46544  fvconst0ci  46545  fvconstdomi  46546  ipolub00  46638