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

Theorem ectocld 8724
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 244 . . 3 ((𝜒𝑥𝐵) → (𝐴 = [𝑥]𝑅𝜓))
54rexlimdva 3153 . 2 (𝜒 → (∃𝑥𝐵 𝐴 = [𝑥]𝑅𝜓))
6 elqsi 8710 . . 3 (𝐴 ∈ (𝐵 / 𝑅) → ∃𝑥𝐵 𝐴 = [𝑥]𝑅)
7 ectocl.1 . . 3 𝑆 = (𝐵 / 𝑅)
86, 7eleq2s 2856 . 2 (𝐴𝑆 → ∃𝑥𝐵 𝐴 = [𝑥]𝑅)
95, 8impel 507 1 ((𝜒𝐴𝑆) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wrex 3074  [cec 8647   / cqs 8648
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3075  df-qs 8655
This theorem is referenced by:  ectocl  8725  elqsn0  8726  qsdisj  8734  qsel  8736  eqgen  18984  orbsta  19094  sylow1lem3  19383  sylow2alem2  19401  sylow2a  19402  sylow2blem2  19404  frgpup1  19558  frgpup3lem  19560  quscrng  20713  pi1xfr  24421  pi1coghm  24427  vitalilem3  24977  qsdisjALTV  37080  eqvrelqsel  37081
  Copyright terms: Public domain W3C validator