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

Theorem ectocld 8824
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 2745 . . . 4 (𝐴 = [𝑥]𝑅 → (𝜑𝜓))
41, 3syl5ibcom 245 . . 3 ((𝜒𝑥𝐵) → (𝐴 = [𝑥]𝑅𝜓))
54rexlimdva 3155 . 2 (𝜒 → (∃𝑥𝐵 𝐴 = [𝑥]𝑅𝜓))
6 elqsi 8810 . . 3 (𝐴 ∈ (𝐵 / 𝑅) → ∃𝑥𝐵 𝐴 = [𝑥]𝑅)
7 ectocl.1 . . 3 𝑆 = (𝐵 / 𝑅)
86, 7eleq2s 2859 . 2 (𝐴𝑆 → ∃𝑥𝐵 𝐴 = [𝑥]𝑅)
95, 8impel 505 1 ((𝜒𝐴𝑆) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wrex 3070  [cec 8743   / cqs 8744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-qs 8751
This theorem is referenced by:  ectocl  8825  elqsn0  8826  qsdisj  8834  qsel  8836  eqgen  19199  orbsta  19331  sylow1lem3  19618  sylow2alem2  19636  sylow2a  19637  sylow2blem2  19639  frgpup1  19793  frgpup3lem  19795  quscrng  21293  pi1xfr  25088  pi1coghm  25094  vitalilem3  25645  qsdisjALTV  38616  eqvrelqsel  38617
  Copyright terms: Public domain W3C validator