Theorem qsss 8769

Description: A quotient set is a set of subsets of the base set. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)

Hypothesis

Ref	Expression
qsss.1	⊢ (𝜑 → 𝑅 Er 𝐴)

Assertion

Ref	Expression
qsss	⊢ (𝜑 → (𝐴 / 𝑅) ⊆ 𝒫 𝐴)

Proof of Theorem qsss

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3459	. . . 4 ⊢ 𝑥 ∈ V
2	1	elqs 8758	. . 3 ⊢ (𝑥 ∈ (𝐴 / 𝑅) ↔ ∃𝑦 ∈ 𝐴 𝑥 = [𝑦]𝑅)
3		qsss.1	. . . . . . 7 ⊢ (𝜑 → 𝑅 Er 𝐴)
4	3	ecss 8742	. . . . . 6 ⊢ (𝜑 → [𝑦]𝑅 ⊆ 𝐴)
5		sseq1 3962	. . . . . 6 ⊢ (𝑥 = [𝑦]𝑅 → (𝑥 ⊆ 𝐴 ↔ [𝑦]𝑅 ⊆ 𝐴))
6	4, 5	syl5ibrcom 250	. . . . 5 ⊢ (𝜑 → (𝑥 = [𝑦]𝑅 → 𝑥 ⊆ 𝐴))
7		velpw 4567	. . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
8	6, 7	imbitrrdi 255	. . . 4 ⊢ (𝜑 → (𝑥 = [𝑦]𝑅 → 𝑥 ∈ 𝒫 𝐴))
9	8	rexlimdvw 3171	. . 3 ⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝑥 = [𝑦]𝑅 → 𝑥 ∈ 𝒫 𝐴))
10	2, 9	biimtrid 245	. 2 ⊢ (𝜑 → (𝑥 ∈ (𝐴 / 𝑅) → 𝑥 ∈ 𝒫 𝐴))
11	10	ssrdv 3943	1 ⊢ (𝜑 → (𝐴 / 𝑅) ⊆ 𝒫 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2143  ∃wrex 3089   ⊆ wss 3905  𝒫 cpw 4562   Er wer 8687  [cec 8688   / cqs 8689

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-cnv 5669  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-er 8690  df-ec 8692  df-qs 8696

This theorem is used by:  nrex1  11053  wuncn  11159  qshash  15884  lagsubg2  19269  lagsubg  19270  ghmqusnsg  19356  ghmquskerlem3  19360  ghmqusker  19361  orbsta2  19388  sylow1lem3  19674  sylow2alem2  19692  sylow2a  19693  sylow2blem2  19695  sylow2blem3  19696  sylow3lem3  19703  sylow3lem4  19704  rhmqusnsg  21434  vitalilem5  25780  vitali  25781  qerclwwlknfi  30433  lmhmqusker  33735  rhmquskerlem  33742  prjspnssbas  43381