Theorem ecexg 8704

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3453  {csn 4587   “ cima 5662  [cec 8698

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 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402  ax-un 7740

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ec 8702

This theorem is used by:  elecex  8751  eroveu  8816  erov  8818  addsrpr  11088  mulsrpr  11089  quslem  17635  eqgen  19312  qusghm  19388  ghmquskerco  19417  sylow2blem1  19753  vrgpval  19900  rngqiprngimf1  21509  znzrhval  21765  qustgpopn  24352  qustgplem  24353  elpi1  25279  pi1xfrval  25288  pi1xfrcnvlem  25290  pi1xfrcnv  25291  pi1cof  25293  pi1coval  25294  tgjustr  28823  rlocf1  33722  qusker  33797  qusvscpbl  33799  qusvsval  33800  qusrn  33846  zringfrac  33972  pstmfval  34414  fvline  36732  dmqmap  39209  qmapeldisjsim  39616