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

Theorem ectocld 7397
Description: Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.)
Hypotheses
Ref Expression
ectocl.1
ectocl.2
ectocld.3
Assertion
Ref Expression
ectocld
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem ectocld
StepHypRef Expression
1 elqsi 7384 . . . 4
2 ectocl.1 . . . 4
31, 2eleq2s 2565 . . 3
4 ectocld.3 . . . . 5
5 ectocl.2 . . . . . 6
65eqcoms 2469 . . . . 5
74, 6syl5ibcom 220 . . . 4
87rexlimdva 2949 . . 3
93, 8syl5 32 . 2
109imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  E.wrex 2808  [cec 7328  /.cqs 7329
This theorem is referenced by:  ectocl  7398  elqsn0  7399  qsdisj  7407  qsel  7409  eqgen  16254  orbsta  16351  sylow1lem3  16620  sylow2alem2  16638  sylow2a  16639  sylow2blem2  16641  frgpup1  16793  frgpup3lem  16795  quscrng  17888  pi1xfr  21555  pi1coghm  21561  vitalilem3  22019
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-qs 7336
  Copyright terms: Public domain W3C validator