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

Theorem str0 14879
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 4525 . . 3  |-  (/)  e.  _V
2 str0.a . . 3  |-  F  = Slot 
I
31, 2strfvn 14856 . 2  |-  ( F `
 (/) )  =  (
(/) `  I )
4 0fv 5881 . 2  |-  ( (/) `  I )  =  (/)
53, 4eqtr2i 2432 1  |-  (/)  =  ( F `  (/) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405   (/)c0 3737   ` cfv 5568  Slot cslot 14838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-iota 5532  df-fun 5570  df-fv 5576  df-slot 14843
This theorem is referenced by:  base0  14880  strfvi  14881  setsnid  14883  resslem  14899  oppchomfval  15325  fuchom  15572  xpchomfval  15770  xpccofval  15773  0pos  15906  oduleval  16083  frmdplusg  16344  oppgplusfval  16705  symgplusg  16736  mgpplusg  17463  opprmulfval  17592  sralem  18141  srasca  18145  sravsca  18146  sraip  18147  psrplusg  18352  psrmulr  18355  psrvscafval  18361  opsrle  18458  ply1plusgfvi  18601  psr1sca2  18610  ply1sca2  18613  zlmlem  18852  zlmvsca  18857  thlle  19024  thloc  19026  resstopn  19978  tnglem  21444  tngds  21452  ttglem  24583  resvlem  28260  mendplusgfval  35478  mendmulrfval  35480  mendsca  35482  mendvscafval  35483
  Copyright terms: Public domain W3C validator