Theorem ecexg 8705

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451  {csn 4584   “ cima 5654  [cec 8699

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 2733  ax-sep 5249  ax-pr 5391  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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ec 8703

This theorem is used by:  elecex  8752  eroveu  8817  erov  8819  addsrpr  11141  mulsrpr  11142  quslem  17695  eqgen  19373  qusghm  19449  ghmquskerco  19478  sylow2blem1  19814  vrgpval  19961  rngqiprngimf1  21576  znzrhval  21832  qustgpopn  24419  qustgplem  24420  elpi1  25346  pi1xfrval  25355  pi1xfrcnvlem  25357  pi1xfrcnv  25358  pi1cof  25360  pi1coval  25361  tgjustr  28918  rlocf1  33817  qusker  33892  qusvscpbl  33894  qusvsval  33895  qusrn  33942  zringfrac  34068  pstmfval  34510  fvline  36879  dmqmap  39353  qmapeldisjsim  39760