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

Theorem ndmfv 6682
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.
StepHypRef Expression
1 euex 2661 . . . . 5 (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2 eldmg 5744 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
31, 2syl5ibr 249 . . . 4 (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥𝐴 ∈ dom 𝐹))
43con3d 155 . . 3 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5 tz6.12-2 6642 . . 3 (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹𝐴) = ∅)
64, 5syl6 35 . 2 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
7 fvprc 6645 . . 3 𝐴 ∈ V → (𝐹𝐴) = ∅)
87a1d 25 . 2 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
96, 8pm2.61i 185 1 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wex 1781  wcel 2114  ∃!weu 2652  Vcvv 3469  c0 4265   class class class wbr 5042  dom cdm 5532  cfv 6334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-nul 5186  ax-pow 5243
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-dm 5542  df-iota 6293  df-fv 6342
This theorem is referenced by:  ndmfvrcl  6683  elfvdm  6684  nfvres  6688  fvfundmfvn0  6690  0fv  6691  funfv  6732  fvun1  6736  fvco4i  6744  fvmpti  6749  mptrcl  6759  fvmptss  6762  fvmptex  6764  fvmptnf  6772  fvmptss2  6775  elfvmptrab1  6777  fvopab4ndm  6779  f0cli  6846  funiunfv  6990  ovprc  7178  oprssdm  7314  nssdmovg  7315  ndmovg  7316  1st2val  7703  2nd2val  7704  brovpreldm  7771  smofvon2  7980  rdgsucmptnf  8052  frsucmptn  8061  brwitnlem  8119  undifixp  8485  r1tr  9193  rankvaln  9216  cardidm  9376  carden2a  9383  carden2b  9384  carddomi2  9387  sdomsdomcardi  9388  pm54.43lem  9417  alephcard  9485  alephnbtwn  9486  alephgeom  9497  cfub  9660  cardcf  9663  cflecard  9664  cfle  9665  cflim2  9674  cfidm  9686  itunisuc  9830  itunitc1  9831  ituniiun  9833  alephadd  9988  alephreg  9993  pwcfsdom  9994  cfpwsdom  9995  adderpq  10367  mulerpq  10368  uzssz  12252  ltweuz  13324  wrdsymb0  13892  lsw0  13908  swrd00  13997  swrd0  14011  pfx00  14027  pfx0  14028  sumz  15070  sumss  15072  sumnul  15106  prod1  15289  prodss  15292  divsfval  16811  cidpropd  16971  lubval  17585  glbval  17598  joinval  17606  meetval  17620  gsumpropd2lem  17880  mulgfval  18217  mpfrcl  20755  iscnp2  21842  setsmstopn  23083  tngtopn  23254  dvbsss  24503  perfdvf  24504  dchrrcl  25822  structiedg0val  26813  snstriedgval  26829  rgrx0nd  27382  vsfval  28414  dmadjrnb  29687  hmdmadj  29721  funeldmb  33080  rdgprc0  33112  soseq  33170  nofv  33238  sltres  33243  noseponlem  33245  noextenddif  33249  noextendlt  33250  noextendgt  33251  nolesgn2ores  33253  fvnobday  33257  nosepdmlem  33261  nosepssdm  33264  nosupbnd1lem3  33284  nosupbnd1lem5  33286  nosupbnd2lem1  33289  fullfunfv  33482  linedegen  33678  bj-inftyexpitaudisj  34581  bj-inftyexpidisj  34586  bj-fvimacnv0  34662  dibvalrel  38421  dicvalrelN  38443  dihvalrel  38537  itgocn  40042  r1rankcld  40877  grur1cld  40878  uz0  41992  climfveq  42254  climfveqf  42265  afv2ndeffv0  43759  fvmptrabdm  43792
  Copyright terms: Public domain W3C validator