Theorem ectocld 8719

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

Step	Hyp	Ref	Expression
1		ectocld.3	. . . 4 ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑)
2		ectocl.2	. . . . 5 ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	eqcoms 2744	. . . 4 ⊢ (𝐴 = [𝑥]𝑅 → (𝜑 ↔ 𝜓))
4	1, 3	syl5ibcom 245	. . 3 ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → (𝐴 = [𝑥]𝑅 → 𝜓))
5	4	rexlimdva 3137	. 2 ⊢ (𝜒 → (∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅 → 𝜓))
6		elqsi 8703	. . 3 ⊢ (𝐴 ∈ (𝐵 / 𝑅) → ∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅)
7		ectocl.1	. . 3 ⊢ 𝑆 = (𝐵 / 𝑅)
8	6, 7	eleq2s 2854	. 2 ⊢ (𝐴 ∈ 𝑆 → ∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅)
9	5, 8	impel 505	1 ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃wrex 3060  [cec 8633   / cqs 8634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-qs 8641

This theorem is referenced by:  ectocl  8720  elqsn0  8721  qsdisj  8731  qsel  8733  eqgen  19110  orbsta  19242  sylow1lem3  19529  sylow2alem2  19547  sylow2a  19548  sylow2blem2  19550  frgpup1  19704  frgpup3lem  19706  quscrng  21238  pi1xfr  25011  pi1coghm  25017  vitalilem3  25567  qsdisjALTV  38868  eqvrelqsel  38869