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

Theorem ectocld 8162
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 2780 . . . 4 (𝐴 = [𝑥]𝑅 → (𝜑𝜓))
41, 3syl5ibcom 237 . . 3 ((𝜒𝑥𝐵) → (𝐴 = [𝑥]𝑅𝜓))
54rexlimdva 3223 . 2 (𝜒 → (∃𝑥𝐵 𝐴 = [𝑥]𝑅𝜓))
6 elqsi 8148 . . 3 (𝐴 ∈ (𝐵 / 𝑅) → ∃𝑥𝐵 𝐴 = [𝑥]𝑅)
7 ectocl.1 . . 3 𝑆 = (𝐵 / 𝑅)
86, 7eleq2s 2878 . 2 (𝐴𝑆 → ∃𝑥𝐵 𝐴 = [𝑥]𝑅)
95, 8impel 498 1 ((𝜒𝐴𝑆) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2050  wrex 3083  [cec 8085   / cqs 8086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-qs 8093
This theorem is referenced by:  ectocl  8163  elqsn0  8164  qsdisj  8172  qsel  8174  eqgen  18128  orbsta  18226  sylow1lem3  18498  sylow2alem2  18516  sylow2a  18517  sylow2blem2  18519  frgpup1  18673  frgpup3lem  18675  quscrng  19746  pi1xfr  23374  pi1coghm  23380  vitalilem3  23926  qsdisjALTV  35324  eqvrelqsel  35325
  Copyright terms: Public domain W3C validator