MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ecexg Structured version   Visualization version   GIF version

Theorem ecexg 8400
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
StepHypRef Expression
1 df-ec 8398 . 2 [𝐴]𝑅 = (𝑅 “ {𝐴})
2 imaexg 7698 . 2 (𝑅𝐵 → (𝑅 “ {𝐴}) ∈ V)
31, 2eqeltrid 2842 1 (𝑅𝐵 → [𝐴]𝑅 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  Vcvv 3413  {csn 4546  cima 5559  [cec 8394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5197  ax-nul 5204  ax-pr 5327  ax-un 7528
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3415  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-br 5059  df-opab 5121  df-xp 5562  df-cnv 5564  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-ec 8398
This theorem is referenced by:  ecelqsg  8459  uniqs  8464  eroveu  8499  erov  8501  addsrpr  10694  mulsrpr  10695  quslem  17053  eqgen  18602  qusghm  18664  sylow2blem1  19014  vrgpval  19162  znzrhval  20516  qustgpopn  23022  qustgplem  23023  elpi1  23947  pi1xfrval  23956  pi1xfrcnvlem  23958  pi1xfrcnv  23959  pi1cof  23961  pi1coval  23962  tgjustr  26570  qusker  31268  qusvscpbl  31270  qusscaval  31271  pstmfval  31565  fvline  34188  ecex2  36205
  Copyright terms: Public domain W3C validator