Theorem ecexg 8707

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3458  {csn 4594   “ cima 5669  [cec 8701

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-xp 5672  df-cnv 5674  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-ec 8705

This theorem is used by:  elecex  8754  eroveu  8819  erov  8821  addsrpr  11078  mulsrpr  11079  quslem  17622  eqgen  19280  qusghm  19356  ghmquskerco  19385  sylow2blem1  19721  vrgpval  19868  rngqiprngimf1  21477  znzrhval  21733  qustgpopn  24314  qustgplem  24315  elpi1  25241  pi1xfrval  25250  pi1xfrcnvlem  25252  pi1xfrcnv  25253  pi1cof  25255  pi1coval  25256  tgjustr  28780  rlocf1  33625  qusker  33700  qusvscpbl  33702  qusvsval  33703  qusrn  33749  zringfrac  33875  pstmfval  34317  fvline  36657  dmqmap  39143  qmapeldisjsim  39550