Theorem ndmfv 6360

Description: The value of a class outside its domain is the empty set. (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 2642	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5458	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	syl5ibr 236	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 149	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6324	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6327	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 25	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 176	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1631  ∃wex 1852   ∈ wcel 2145  ∃!weu 2618  Vcvv 3351  ∅c0 4064   class class class wbr 4787  dom cdm 5250  ‘cfv 6032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4924  ax-pow 4975

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-dm 5260  df-iota 5995  df-fv 6040

This theorem is referenced by:  ndmfvrcl  6361  elfvdm  6362  nfvres  6366  fvfundmfvn0  6368  0fv  6369  funfv  6408  fvun1  6412  fvco4i  6419  fvmpti  6424  mptrcl  6432  fvmptss  6435  fvmptex  6437  fvmptnf  6445  fvmptss2  6447  elfvmptrab1  6448  fvopab4ndm  6450  f0cli  6514  funiunfv  6650  ovprc  6829  oprssdm  6963  nssdmovg  6964  ndmovg  6965  1st2val  7344  2nd2val  7345  brovpreldm  7406  curry1val  7422  curry2val  7426  smofvon2  7607  rdgsucmptnf  7679  frsucmptn  7688  brwitnlem  7742  undifixp  8099  r1tr  8804  rankvaln  8827  cardidm  8986  carden2a  8993  carden2b  8994  carddomi2  8997  sdomsdomcardi  8998  pm54.43lem  9026  alephcard  9094  alephnbtwn  9095  alephgeom  9106  cfub  9274  cardcf  9277  cflecard  9278  cfle  9279  cflim2  9288  cfidm  9300  itunisuc  9444  itunitc1  9445  ituniiun  9447  alephadd  9602  alephreg  9607  pwcfsdom  9608  cfpwsdom  9609  adderpq  9981  mulerpq  9982  uzssz  11909  ltweuz  12969  wrdsymb0  13536  lsw0  13550  swrd00  13627  swrd0  13644  sumz  14662  sumss  14664  sumnul  14700  prod1  14882  prodss  14885  divsfval  16416  cidpropd  16578  arwval  16901  coafval  16922  lubval  17193  glbval  17206  joinval  17214  meetval  17228  gsumpropd2lem  17482  mpfrcl  19734  iscnp2  21265  setsmstopn  22504  tngtopn  22675  pcofval  23030  dvbsss  23887  perfdvf  23888  dchrrcl  25187  eleenn  25998  structiedg0val  26133  snstriedgval  26152  rgrx0nd  26726  vsfval  27829  dmadjrnb  29106  hmdmadj  29140  funeldmb  32000  rdgprc0  32036  soseq  32092  nofv  32148  sltres  32153  noseponlem  32155  noextenddif  32159  noextendlt  32160  noextendgt  32161  nolesgn2ores  32163  fvnobday  32167  nosepdmlem  32171  nosepssdm  32174  nosupbnd1lem3  32194  nosupbnd1lem5  32196  nosupbnd2lem1  32199  fullfunfv  32392  linedegen  32588  bj-inftyexpidisj  33435  dibvalrel  36974  dicvalrelN  36996  dihvalrel  37090  itgocn  38261  uz0  40156  climfveq  40420  climfveqf  40431  fvmptrabdm  41836  pfx00  41913  pfx0  41914  setrec2lem1  42969