Theorem ecexg 8678

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450  {csn 4592   “ cima 5644  [cec 8672

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-ec 8676

This theorem is referenced by:  elecex  8724  eroveu  8788  erov  8790  addsrpr  11035  mulsrpr  11036  quslem  17513  eqgen  19120  qusghm  19194  ghmquskerco  19223  sylow2blem1  19557  vrgpval  19704  rngqiprngimf1  21217  znzrhval  21463  qustgpopn  24014  qustgplem  24015  elpi1  24952  pi1xfrval  24961  pi1xfrcnvlem  24963  pi1xfrcnv  24964  pi1cof  24966  pi1coval  24967  tgjustr  28408  rlocf1  33231  qusker  33327  qusvscpbl  33329  qusvsval  33330  qusrn  33387  zringfrac  33532  pstmfval  33893  fvline  36139