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

Theorem ectocld 6726
Description: Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.)
Hypotheses
Ref Expression
ectocl.1  |-  S  =  ( B /. R
)
ectocl.2  |-  ( [ x ] R  =  A  ->  ( ph  <->  ps ) )
ectocld.3  |-  ( ( ch  /\  x  e.  B )  ->  ph )
Assertion
Ref Expression
ectocld  |-  ( ( ch  /\  A  e.  S )  ->  ps )
Distinct variable groups:    x, A    x, B    x, R    ps, x    ch, x
Allowed substitution hints:    ph( x)    S( x)

Proof of Theorem ectocld
StepHypRef Expression
1 elqsi 6713 . . . 4  |-  ( A  e.  ( B /. R )  ->  E. x  e.  B  A  =  [ x ] R
)
2 ectocl.1 . . . 4  |-  S  =  ( B /. R
)
31, 2eleq2s 2375 . . 3  |-  ( A  e.  S  ->  E. x  e.  B  A  =  [ x ] R
)
4 ectocld.3 . . . . 5  |-  ( ( ch  /\  x  e.  B )  ->  ph )
5 ectocl.2 . . . . . 6  |-  ( [ x ] R  =  A  ->  ( ph  <->  ps ) )
65eqcoms 2286 . . . . 5  |-  ( A  =  [ x ] R  ->  ( ph  <->  ps )
)
74, 6syl5ibcom 211 . . . 4  |-  ( ( ch  /\  x  e.  B )  ->  ( A  =  [ x ] R  ->  ps )
)
87rexlimdva 2667 . . 3  |-  ( ch 
->  ( E. x  e.  B  A  =  [
x ] R  ->  ps ) )
93, 8syl5 28 . 2  |-  ( ch 
->  ( A  e.  S  ->  ps ) )
109imp 418 1  |-  ( ( ch  /\  A  e.  S )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   E.wrex 2544   [cec 6658   /.cqs 6659
This theorem is referenced by:  ectocl  6727  elqsn0  6728  qsdisj  6736  qsel  6738  eqgen  14670  orbsta  14767  sylow1lem3  14911  sylow2alem2  14929  sylow2a  14930  sylow2blem2  14932  frgpup1  15084  frgpup3lem  15086  divscrng  15992  pi1xfr  18553  pi1coghm  18559  vitalilem3  18965
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-v 2790  df-qs 6666
  Copyright terms: Public domain W3C validator