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

Theorem ectocld 6930
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 6917 . . . 4  |-  ( A  e.  ( B /. R )  ->  E. x  e.  B  A  =  [ x ] R
)
2 ectocl.1 . . . 4  |-  S  =  ( B /. R
)
31, 2eleq2s 2496 . . 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 2407 . . . . 5  |-  ( A  =  [ x ] R  ->  ( ph  <->  ps )
)
74, 6syl5ibcom 212 . . . 4  |-  ( ( ch  /\  x  e.  B )  ->  ( A  =  [ x ] R  ->  ps )
)
87rexlimdva 2790 . . 3  |-  ( ch 
->  ( E. x  e.  B  A  =  [
x ] R  ->  ps ) )
93, 8syl5 30 . 2  |-  ( ch 
->  ( A  e.  S  ->  ps ) )
109imp 419 1  |-  ( ( ch  /\  A  e.  S )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1721   E.wrex 2667   [cec 6862   /.cqs 6863
This theorem is referenced by:  ectocl  6931  elqsn0  6932  qsdisj  6940  qsel  6942  eqgen  14948  orbsta  15045  sylow1lem3  15189  sylow2alem2  15207  sylow2a  15208  sylow2blem2  15210  frgpup1  15362  frgpup3lem  15364  divscrng  16266  pi1xfr  19033  pi1coghm  19039  vitalilem3  19455
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-v 2918  df-qs 6870
  Copyright terms: Public domain W3C validator