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

Theorem ectocld 8778
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:   𝑥,𝐴   𝑥,𝐵   𝑥,𝑅   𝜓,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑆(𝑥)

Proof of Theorem ectocld
StepHypRef Expression
1 ectocld.3 . . . 4 ((𝜒𝑥𝐵) → 𝜑)
2 ectocl.2 . . . . 5 ([𝑥]𝑅 = 𝐴 → (𝜑𝜓))
32eqcoms 2741 . . . 4 (𝐴 = [𝑥]𝑅 → (𝜑𝜓))
41, 3syl5ibcom 244 . . 3 ((𝜒𝑥𝐵) → (𝐴 = [𝑥]𝑅𝜓))
54rexlimdva 3156 . 2 (𝜒 → (∃𝑥𝐵 𝐴 = [𝑥]𝑅𝜓))
6 elqsi 8764 . . 3 (𝐴 ∈ (𝐵 / 𝑅) → ∃𝑥𝐵 𝐴 = [𝑥]𝑅)
7 ectocl.1 . . 3 𝑆 = (𝐵 / 𝑅)
86, 7eleq2s 2852 . 2 (𝐴𝑆 → ∃𝑥𝐵 𝐴 = [𝑥]𝑅)
95, 8impel 507 1 ((𝜒𝐴𝑆) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wrex 3071  [cec 8701   / cqs 8702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-qs 8709
This theorem is referenced by:  ectocl  8779  elqsn0  8780  qsdisj  8788  qsel  8790  eqgen  19061  orbsta  19177  sylow1lem3  19468  sylow2alem2  19486  sylow2a  19487  sylow2blem2  19489  frgpup1  19643  frgpup3lem  19645  quscrng  20878  pi1xfr  24571  pi1coghm  24577  vitalilem3  25127  qsdisjALTV  37485  eqvrelqsel  37486
  Copyright terms: Public domain W3C validator