Theorem ecexg 8749

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 8747	. 2 ⊢ [𝐴]𝑅 = (𝑅 “ {𝐴})
2		imaexg 7935	. 2 ⊢ (𝑅 ∈ 𝐵 → (𝑅 “ {𝐴}) ∈ V)
3	1, 2	eqeltrid 2845	1 ⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480  {csn 4626   “ cima 5688  [cec 8743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ec 8747

This theorem is referenced by:  ecelqsg  8812  uniqs  8817  eroveu  8852  erov  8854  addsrpr  11115  mulsrpr  11116  quslem  17588  eqgen  19199  qusghm  19273  ghmquskerco  19302  sylow2blem1  19638  vrgpval  19785  rngqiprngimf1  21310  znzrhval  21565  qustgpopn  24128  qustgplem  24129  elpi1  25078  pi1xfrval  25087  pi1xfrcnvlem  25089  pi1xfrcnv  25090  pi1cof  25092  pi1coval  25093  tgjustr  28482  rlocf1  33277  qusker  33377  qusvscpbl  33379  qusvsval  33380  qusrn  33437  zringfrac  33582  pstmfval  33895  fvline  36145  ecex2  38329