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

Theorem ndmfv 6256
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 2522 . . . . 5 (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2 eldmg 5351 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
31, 2syl5ibr 236 . . . 4 (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥𝐴 ∈ dom 𝐹))
43con3d 148 . . 3 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5 tz6.12-2 6220 . . 3 (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹𝐴) = ∅)
64, 5syl6 35 . 2 (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹𝐴) = ∅))
7 fvprc 6223 . . 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 1523  wex 1744  wcel 2030  ∃!weu 2498  Vcvv 3231  c0 3948   class class class wbr 4685  dom cdm 5143  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822  ax-pow 4873
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-dm 5153  df-iota 5889  df-fv 5934
This theorem is referenced by:  ndmfvrcl  6257  elfvdm  6258  nfvres  6262  fvfundmfvn0  6264  0fv  6265  funfv  6304  fvun1  6308  fvco4i  6315  fvmpti  6320  mptrcl  6328  fvmptss  6331  fvmptex  6333  fvmptnf  6341  fvmptss2  6343  elfvmptrab1  6344  fvopab4ndm  6346  f0cli  6410  funiunfv  6546  ovprc  6723  oprssdm  6857  nssdmovg  6858  ndmovg  6859  1st2val  7238  2nd2val  7239  brovpreldm  7299  curry1val  7315  curry2val  7319  smofvon2  7498  rdgsucmptnf  7570  frsucmptn  7579  brwitnlem  7632  undifixp  7986  r1tr  8677  rankvaln  8700  cardidm  8823  carden2a  8830  carden2b  8831  carddomi2  8834  sdomsdomcardi  8835  pm54.43lem  8863  alephcard  8931  alephnbtwn  8932  alephgeom  8943  cfub  9109  cardcf  9112  cflecard  9113  cfle  9114  cflim2  9123  cfidm  9135  itunisuc  9279  itunitc1  9280  ituniiun  9282  alephadd  9437  alephreg  9442  pwcfsdom  9443  cfpwsdom  9444  adderpq  9816  mulerpq  9817  uzssz  11745  ltweuz  12800  wrdsymb0  13371  lsw0  13385  swrd00  13463  swrd0  13480  sumz  14497  sumss  14499  sumnul  14535  prod1  14718  prodss  14721  divsfval  16254  cidpropd  16417  arwval  16740  coafval  16761  lubval  17031  glbval  17044  joinval  17052  meetval  17066  gsumpropd2lem  17320  mpfrcl  19566  iscnp2  21091  setsmstopn  22330  tngtopn  22501  pcofval  22856  dvbsss  23711  perfdvf  23712  dchrrcl  25010  eleenn  25821  structiedg0val  25956  snstriedgval  25975  rgrx0nd  26546  vsfval  27616  dmadjrnb  28893  hmdmadj  28927  funeldmb  31787  rdgprc0  31823  soseq  31879  nofv  31935  sltres  31940  noseponlem  31942  noextenddif  31946  noextendlt  31947  noextendgt  31948  nolesgn2ores  31950  fvnobday  31954  nosepdmlem  31958  nosepssdm  31961  nosupbnd1lem3  31981  nosupbnd1lem5  31983  nosupbnd2lem1  31986  fullfunfv  32179  linedegen  32375  bj-inftyexpidisj  33227  dibvalrel  36769  dicvalrelN  36791  dihvalrel  36885  itgocn  38051  uz0  39952  climfveq  40219  climfveqf  40230  fvmptrabdm  41632  pfx00  41709  pfx0  41710  setrec2lem1  42765
  Copyright terms: Public domain W3C validator