MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  str0 Structured version   Unicode version

Theorem str0 14331
Description: All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
Hypothesis
Ref Expression
str0.a  |-  F  = Slot 
I
Assertion
Ref Expression
str0  |-  (/)  =  ( F `  (/) )

Proof of Theorem str0
StepHypRef Expression
1 0ex 4531 . . 3  |-  (/)  e.  _V
2 str0.a . . 3  |-  F  = Slot 
I
31, 2strfvn 14310 . 2  |-  ( F `
 (/) )  =  (
(/) `  I )
4 0fv 5833 . 2  |-  ( (/) `  I )  =  (/)
53, 4eqtr2i 2484 1  |-  (/)  =  ( F `  (/) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370   (/)c0 3746   ` cfv 5527  Slot cslot 14292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-br 4402  df-opab 4460  df-mpt 4461  df-id 4745  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-iota 5490  df-fun 5529  df-fv 5535  df-slot 14297
This theorem is referenced by:  base0  14332  strfvi  14333  setsnid  14335  resslem  14351  oppchomfval  14773  fuchom  14991  xpchomfval  15109  xpccofval  15112  0pos  15244  oduleval  15421  frmdplusg  15652  oppgplusfval  15983  symgplusg  16014  mgpplusg  16718  opprmulfval  16841  sralem  17382  srasca  17386  sravsca  17387  sraip  17388  psrplusg  17576  psrmulr  17579  psrvscafval  17585  opsrle  17682  ply1plusgfvi  17821  psr1sca2  17830  ply1sca2  17833  zlmlem  18074  zlmvsca  18079  thlle  18248  thloc  18250  resstopn  18923  tnglem  20359  tngds  20367  ttglem  23275  resvlem  26445  mendplusgfval  29691  mendmulrfval  29693  mendsca  29695  mendvscafval  29696
  Copyright terms: Public domain W3C validator