MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ndmfv Structured version   Visualization version   GIF version

Theorem ndmfv 6205
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.
StepHypRef Expression
1 euex 2492 . . . . 5 (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2 eldmg 5308 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
31, 2syl5ibr 236 . . . 4 (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥𝐴 ∈ dom 𝐹))
43con3d 148 . . 3 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5 tz6.12-2 6169 . . 3 (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹𝐴) = ∅)
64, 5syl6 35 . 2 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
7 fvprc 6172 . . 3 𝐴 ∈ V → (𝐹𝐴) = ∅)
87a1d 25 . 2 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
96, 8pm2.61i 176 1 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1481  wex 1702  wcel 1988  ∃!weu 2468  Vcvv 3195  c0 3907   class class class wbr 4644  dom cdm 5104  cfv 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-nul 4780  ax-pow 4834
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-dm 5114  df-iota 5839  df-fv 5884
This theorem is referenced by:  ndmfvrcl  6206  elfvdm  6207  nfvres  6211  fvfundmfvn0  6213  0fv  6214  funfv  6252  fvun1  6256  fvco4i  6263  fvmpti  6268  mptrcl  6276  fvmptss  6279  fvmptex  6281  fvmptnf  6288  fvmptss2  6290  elfvmptrab1  6291  fvopab4ndm  6293  f0cli  6356  funiunfv  6491  ovprc  6668  oprssdm  6800  nssdmovg  6801  ndmovg  6802  1st2val  7179  2nd2val  7180  brovpreldm  7239  curry1val  7255  curry2val  7259  smofvon2  7438  rdgsucmptnf  7510  frsucmptn  7519  brwitnlem  7572  undifixp  7929  r1tr  8624  rankvaln  8647  cardidm  8770  carden2a  8777  carden2b  8778  carddomi2  8781  sdomsdomcardi  8782  pm54.43lem  8810  alephcard  8878  alephnbtwn  8879  alephgeom  8890  cfub  9056  cardcf  9059  cflecard  9060  cfle  9061  cflim2  9070  cfidm  9082  itunisuc  9226  itunitc1  9227  ituniiun  9229  alephadd  9384  alephreg  9389  pwcfsdom  9390  cfpwsdom  9391  adderpq  9763  mulerpq  9764  uzssz  11692  ltweuz  12743  wrdsymb0  13322  lsw0  13335  swrd00  13400  swrd0  13416  sumz  14434  sumss  14436  sumnul  14472  prod1  14655  prodss  14658  divsfval  16188  cidpropd  16351  arwval  16674  coafval  16695  lubval  16965  glbval  16978  joinval  16986  meetval  17000  gsumpropd2lem  17254  mpfrcl  19499  iscnp2  21024  setsmstopn  22264  tngtopn  22435  pcofval  22791  dvbsss  23647  perfdvf  23648  dchrrcl  24946  eleenn  25757  structiedg0val  25892  snstriedgval  25911  rgrx0nd  26471  vsfval  27458  dmadjrnb  28735  hmdmadj  28769  funeldmb  31637  rdgprc0  31673  soseq  31725  nofv  31784  sltres  31789  noseponlem  31791  noextenddif  31795  noextendlt  31796  noextendgt  31797  nolesgn2ores  31799  fvnobday  31803  nosepdmlem  31807  nosepssdm  31810  nosupbnd1lem3  31830  nosupbnd1lem5  31832  nosupbnd2lem1  31835  fullfunfv  32029  linedegen  32225  bj-inftyexpidisj  33068  dibvalrel  36271  dicvalrelN  36293  dihvalrel  36387  itgocn  37553  uz0  39452  climfveq  39701  climfveqf  39712  pfx00  41149  pfx0  41150  setrec2lem1  42205
  Copyright terms: Public domain W3C validator