Theorem qsss 8713

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 3444	. . . 4 ⊢ 𝑥 ∈ V
2	1	elqs 8702	. . 3 ⊢ (𝑥 ∈ (𝐴 / 𝑅) ↔ ∃𝑦 ∈ 𝐴 𝑥 = [𝑦]𝑅)
3		qsss.1	. . . . . . 7 ⊢ (𝜑 → 𝑅 Er 𝐴)
4	3	ecss 8686	. . . . . 6 ⊢ (𝜑 → [𝑦]𝑅 ⊆ 𝐴)
5		sseq1 3959	. . . . . 6 ⊢ (𝑥 = [𝑦]𝑅 → (𝑥 ⊆ 𝐴 ↔ [𝑦]𝑅 ⊆ 𝐴))
6	4, 5	syl5ibrcom 247	. . . . 5 ⊢ (𝜑 → (𝑥 = [𝑦]𝑅 → 𝑥 ⊆ 𝐴))
7		velpw 4559	. . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
8	6, 7	imbitrrdi 252	. . . 4 ⊢ (𝜑 → (𝑥 = [𝑦]𝑅 → 𝑥 ∈ 𝒫 𝐴))
9	8	rexlimdvw 3142	. . 3 ⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝑥 = [𝑦]𝑅 → 𝑥 ∈ 𝒫 𝐴))
10	2, 9	biimtrid 242	. 2 ⊢ (𝜑 → (𝑥 ∈ (𝐴 / 𝑅) → 𝑥 ∈ 𝒫 𝐴))
11	10	ssrdv 3939	1 ⊢ (𝜑 → (𝐴 / 𝑅) ⊆ 𝒫 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∃wrex 3060   ⊆ wss 3901  𝒫 cpw 4554   Er wer 8632  [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  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-er 8635  df-ec 8637  df-qs 8641

This theorem is referenced by:  nrex1  10975  wuncn  11081  qshash  15750  lagsubg2  19123  lagsubg  19124  ghmqusnsg  19211  ghmquskerlem3  19215  ghmqusker  19216  orbsta2  19243  sylow1lem3  19529  sylow2alem2  19547  sylow2a  19548  sylow2blem2  19550  sylow2blem3  19551  sylow3lem3  19558  sylow3lem4  19559  rhmqusnsg  21240  vitalilem5  25569  vitali  25570  qerclwwlknfi  30148  lmhmqusker  33498  rhmquskerlem  33506  prjspnssbas  42864