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

Theorem ectocld 7701
 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 elqsi 7687 . . . 4 (𝐴 ∈ (𝐵 / 𝑅) → ∃𝑥𝐵 𝐴 = [𝑥]𝑅)
2 ectocl.1 . . . 4 𝑆 = (𝐵 / 𝑅)
31, 2eleq2s 2706 . . 3 (𝐴𝑆 → ∃𝑥𝐵 𝐴 = [𝑥]𝑅)
4 ectocld.3 . . . . 5 ((𝜒𝑥𝐵) → 𝜑)
5 ectocl.2 . . . . . 6 ([𝑥]𝑅 = 𝐴 → (𝜑𝜓))
65eqcoms 2618 . . . . 5 (𝐴 = [𝑥]𝑅 → (𝜑𝜓))
74, 6syl5ibcom 234 . . . 4 ((𝜒𝑥𝐵) → (𝐴 = [𝑥]𝑅𝜓))
87rexlimdva 3013 . . 3 (𝜒 → (∃𝑥𝐵 𝐴 = [𝑥]𝑅𝜓))
93, 8syl5 33 . 2 (𝜒 → (𝐴𝑆𝜓))
109imp 444 1 ((𝜒𝐴𝑆) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∃wrex 2897  [cec 7627   / cqs 7628 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-qs 7635 This theorem is referenced by:  ectocl  7702  elqsn0  7703  qsdisj  7711  qsel  7713  eqgen  17470  orbsta  17569  sylow1lem3  17838  sylow2alem2  17856  sylow2a  17857  sylow2blem2  17859  frgpup1  18011  frgpup3lem  18013  quscrng  19061  pi1xfr  22663  pi1coghm  22669  vitalilem3  23185
 Copyright terms: Public domain W3C validator