Theorem ndmfv 6218

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 2494	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5319	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	syl5ibr 236	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 148	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6182	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6185	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 25	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 176	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483  ∃wex 1704   ∈ wcel 1990  ∃!weu 2470  Vcvv 3200  ∅c0 3915   class class class wbr 4653  dom cdm 5114  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789  ax-pow 4843

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-dm 5124  df-iota 5851  df-fv 5896

This theorem is referenced by:  ndmfvrcl  6219  elfvdm  6220  nfvres  6224  fvfundmfvn0  6226  0fv  6227  funfv  6265  fvun1  6269  fvco4i  6276  fvmpti  6281  mptrcl  6289  fvmptss  6292  fvmptex  6294  fvmptnf  6302  fvmptss2  6304  elfvmptrab1  6305  fvopab4ndm  6307  f0cli  6370  funiunfv  6506  ovprc  6683  oprssdm  6815  nssdmovg  6816  ndmovg  6817  1st2val  7194  2nd2val  7195  brovpreldm  7254  curry1val  7270  curry2val  7274  smofvon2  7453  rdgsucmptnf  7525  frsucmptn  7534  brwitnlem  7587  undifixp  7944  r1tr  8639  rankvaln  8662  cardidm  8785  carden2a  8792  carden2b  8793  carddomi2  8796  sdomsdomcardi  8797  pm54.43lem  8825  alephcard  8893  alephnbtwn  8894  alephgeom  8905  cfub  9071  cardcf  9074  cflecard  9075  cfle  9076  cflim2  9085  cfidm  9097  itunisuc  9241  itunitc1  9242  ituniiun  9244  alephadd  9399  alephreg  9404  pwcfsdom  9405  cfpwsdom  9406  adderpq  9778  mulerpq  9779  uzssz  11707  ltweuz  12760  wrdsymb0  13339  lsw0  13352  swrd00  13418  swrd0  13434  sumz  14453  sumss  14455  sumnul  14491  prod1  14674  prodss  14677  divsfval  16207  cidpropd  16370  arwval  16693  coafval  16714  lubval  16984  glbval  16997  joinval  17005  meetval  17019  gsumpropd2lem  17273  mpfrcl  19518  iscnp2  21043  setsmstopn  22283  tngtopn  22454  pcofval  22810  dvbsss  23666  perfdvf  23667  dchrrcl  24965  eleenn  25776  structiedg0val  25911  snstriedgval  25930  rgrx0nd  26490  vsfval  27488  dmadjrnb  28765  hmdmadj  28799  funeldmb  31661  rdgprc0  31699  soseq  31751  nofv  31810  sltres  31815  noseponlem  31817  noextenddif  31821  noextendlt  31822  noextendgt  31823  nolesgn2ores  31825  fvnobday  31829  nosepdmlem  31833  nosepssdm  31836  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd2lem1  31861  fullfunfv  32054  linedegen  32250  bj-inftyexpidisj  33097  dibvalrel  36452  dicvalrelN  36474  dihvalrel  36568  itgocn  37734  uz0  39639  climfveq  39901  climfveqf  39912  pfx00  41384  pfx0  41385  setrec2lem1  42440