Theorem ecexg 8502

Description: An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.)

Assertion

Ref	Expression
ecexg	⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V)

Proof of Theorem ecexg

Step	Hyp	Ref	Expression
1		df-ec 8500	. 2 ⊢ [𝐴]𝑅 = (𝑅 “ {𝐴})
2		imaexg 7762	. 2 ⊢ (𝑅 ∈ 𝐵 → (𝑅 “ {𝐴}) ∈ V)
3	1, 2	eqeltrid 2843	1 ⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3432  {csn 4561   “ cima 5592  [cec 8496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ec 8500

This theorem is referenced by:  ecelqsg  8561  uniqs  8566  eroveu  8601  erov  8603  addsrpr  10831  mulsrpr  10832  quslem  17254  eqgen  18809  qusghm  18871  sylow2blem1  19225  vrgpval  19373  znzrhval  20754  qustgpopn  23271  qustgplem  23272  elpi1  24208  pi1xfrval  24217  pi1xfrcnvlem  24219  pi1xfrcnv  24220  pi1cof  24222  pi1coval  24223  tgjustr  26835  qusker  31549  qusvscpbl  31551  qusscaval  31552  pstmfval  31846  fvline  34446  ecex2  36463