Theorem ectocld 8831

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 2771	. . . 4 ⊢ (𝐴 = [𝑥]𝑅 → (𝜑 ↔ 𝜓))
4	1, 3	syl5ibcom 248	. . 3 ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → (𝐴 = [𝑥]𝑅 → 𝜓))
5	4	rexlimdva 3167	. 2 ⊢ (𝜒 → (∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅 → 𝜓))
6		elqsi 8814	. . 3 ⊢ (𝐴 ∈ (𝐵 / 𝑅) → ∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅)
7		ectocl.1	. . 3 ⊢ 𝑆 = (𝐵 / 𝑅)
8	6, 7	eleq2s 2882	. 2 ⊢ (𝐴 ∈ 𝑆 → ∃𝑥 ∈ 𝐵 𝐴 = [𝑥]𝑅)
9	5, 8	impel 515	1 ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∃wrex 3090  [cec 8743   / cqs 8744

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-qs 8751

This theorem is used by:  ectocl  8832  elqsn0  8833  qsdisj  8843  qsel  8845  eqgen  19422  orbsta  19557  sylow1lem3  19844  sylow2alem2  19862  sylow2a  19863  sylow2blem2  19865  frgpup1  20019  frgpup3lem  20021  quscrng  21609  pi1xfr  25406  pi1coghm  25412  vitalilem3  25961  qsdisjALTV  39823  eqvrelqsel  39824