Theorem ecexg 8644

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3432  {csn 4562   “ cima 5628  [cec 8638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ec 8642

This theorem is referenced by:  elecex  8691  eroveu  8756  erov  8758  addsrpr  10996  mulsrpr  10997  quslem  17505  eqgen  19154  qusghm  19228  ghmquskerco  19257  sylow2blem1  19593  vrgpval  19740  rngqiprngimf1  21300  znzrhval  21528  qustgpopn  24110  qustgplem  24111  elpi1  25037  pi1xfrval  25046  pi1xfrcnvlem  25048  pi1xfrcnv  25049  pi1cof  25051  pi1coval  25052  tgjustr  28567  rlocf1  33361  qusker  33439  qusvscpbl  33441  qusvsval  33442  qusrn  33499  zringfrac  33644  pstmfval  34087  fvline  36379  dmqmap  38827  qmapeldisjsim  39234