Theorem ndmfv 6813

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 2578	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5810	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	syl5ibr 245	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6771	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6775	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 25	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 182	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539  ∃wex 1782   ∈ wcel 2107  ∃!weu 2569  Vcvv 3433  ∅c0 4257   class class class wbr 5075  dom cdm 5590  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-dm 5600  df-iota 6395  df-fv 6445

This theorem is referenced by:  ndmfvrcl  6814  elfvdm  6815  nfvres  6819  fvfundmfvn0  6821  0fv  6822  funfv  6864  fvun1  6868  fvco4i  6878  fvmpti  6883  mptrcl  6893  fvmptss  6896  fvmptex  6898  fvmptnf  6906  fvmptss2  6909  elfvmptrab1  6911  fvopab4ndm  6913  f0cli  6983  funiunfv  7130  ovprc  7322  oprssdm  7462  nssdmovg  7463  ndmovg  7464  1st2val  7868  2nd2val  7869  brovpreldm  7938  smofvon2  8196  rdgsucmptnf  8269  frsucmptn  8279  brwitnlem  8346  undifixp  8731  r1tr  9543  rankvaln  9566  cardidm  9726  carden2a  9733  carden2b  9734  carddomi2  9737  sdomsdomcardi  9738  pm54.43lem  9767  alephcard  9835  alephnbtwn  9836  alephgeom  9847  cfub  10014  cardcf  10017  cflecard  10018  cfle  10019  cflim2  10028  cfidm  10040  itunisuc  10184  itunitc1  10185  ituniiun  10187  alephadd  10342  alephreg  10347  pwcfsdom  10348  cfpwsdom  10349  adderpq  10721  mulerpq  10722  uzssz  12612  ltweuz  13690  wrdsymb0  14261  lsw0  14277  swrd00  14366  swrd0  14380  pfx00  14396  pfx0  14397  sumz  15443  sumss  15445  sumnul  15481  prod1  15663  prodss  15666  divsfval  17267  cidpropd  17428  lubval  18083  glbval  18096  joinval  18104  meetval  18118  gsumpropd2lem  18372  mulgfval  18711  mpfrcl  21304  iscnp2  22399  setsmstopn  23642  tngtopn  23823  dvbsss  25075  perfdvf  25076  dchrrcl  26397  structiedg0val  27401  snstriedgval  27417  rgrx0nd  27970  vsfval  29004  dmadjrnb  30277  hmdmadj  30311  funeldmb  33746  rdgprc0  33778  soseq  33812  nofv  33869  sltres  33874  noseponlem  33876  noextenddif  33880  noextendlt  33881  noextendgt  33882  nolesgn2ores  33884  nogesgn1ores  33886  fvnobday  33890  nosepdmlem  33895  nosepssdm  33898  nosupbnd1lem3  33922  nosupbnd1lem5  33924  nosupbnd2lem1  33927  noinfbnd1lem3  33937  noinfbnd1lem5  33939  noinfbnd2lem1  33942  newval  34048  leftval  34056  rightval  34057  madess  34068  oldssmade  34069  lrold  34086  fullfunfv  34258  linedegen  34454  bj-inftyexpitaudisj  35385  bj-inftyexpidisj  35390  bj-fvimacnv0  35466  dibvalrel  39184  dicvalrelN  39206  dihvalrel  39300  itgocn  40996  r1rankcld  41856  grur1cld  41857  uz0  42959  climfveq  43217  climfveqf  43228  afv2ndeffv0  44763  fvmptrabdm  44796  fvconstr  46194  fvconstrn0  46195  fvconstr2  46196  fvconst0ci  46197  fvconstdomi  46198  ipolub00  46290