Theorem qsss 8717

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 3434	. . . 4 ⊢ 𝑥 ∈ V
2	1	elqs 8706	. . 3 ⊢ (𝑥 ∈ (𝐴 / 𝑅) ↔ ∃𝑦 ∈ 𝐴 𝑥 = [𝑦]𝑅)
3		qsss.1	. . . . . . 7 ⊢ (𝜑 → 𝑅 Er 𝐴)
4	3	ecss 8690	. . . . . 6 ⊢ (𝜑 → [𝑦]𝑅 ⊆ 𝐴)
5		sseq1 3948	. . . . . 6 ⊢ (𝑥 = [𝑦]𝑅 → (𝑥 ⊆ 𝐴 ↔ [𝑦]𝑅 ⊆ 𝐴))
6	4, 5	syl5ibrcom 247	. . . . 5 ⊢ (𝜑 → (𝑥 = [𝑦]𝑅 → 𝑥 ⊆ 𝐴))
7		velpw 4547	. . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
8	6, 7	imbitrrdi 252	. . . 4 ⊢ (𝜑 → (𝑥 = [𝑦]𝑅 → 𝑥 ∈ 𝒫 𝐴))
9	8	rexlimdvw 3144	. . 3 ⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝑥 = [𝑦]𝑅 → 𝑥 ∈ 𝒫 𝐴))
10	2, 9	biimtrid 242	. 2 ⊢ (𝜑 → (𝑥 ∈ (𝐴 / 𝑅) → 𝑥 ∈ 𝒫 𝐴))
11	10	ssrdv 3928	1 ⊢ (𝜑 → (𝐴 / 𝑅) ⊆ 𝒫 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∃wrex 3062   ⊆ wss 3890  𝒫 cpw 4542   Er wer 8635  [cec 8636   / cqs 8637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5632  df-rel 5633  df-cnv 5634  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-er 8638  df-ec 8640  df-qs 8644

This theorem is referenced by:  nrex1  10982  wuncn  11088  qshash  15785  lagsubg2  19164  lagsubg  19165  ghmqusnsg  19252  ghmquskerlem3  19256  ghmqusker  19257  orbsta2  19284  sylow1lem3  19570  sylow2alem2  19588  sylow2a  19589  sylow2blem2  19591  sylow2blem3  19592  sylow3lem3  19599  sylow3lem4  19600  rhmqusnsg  21279  vitalilem5  25593  vitali  25594  qerclwwlknfi  30162  lmhmqusker  33496  rhmquskerlem  33504  prjspnssbas  43072