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

Theorem ecelqsi 8340
Description: Membership of an equivalence class in a quotient set. (Contributed by NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
Hypothesis
Ref Expression
ecelqsi.1 𝑅 ∈ V
Assertion
Ref Expression
ecelqsi (𝐵𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅))

Proof of Theorem ecelqsi
StepHypRef Expression
1 ecelqsi.1 . 2 𝑅 ∈ V
2 ecelqsg 8339 . 2 ((𝑅 ∈ V ∧ 𝐵𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
31, 2mpan 689 1 (𝐵𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  Vcvv 3469  [cec 8274   / cqs 8275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-xp 5538  df-cnv 5540  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-ec 8278  df-qs 8282
This theorem is referenced by:  ecopqsi  8341  addsrpr  10486  mulsrpr  10487  0r  10491  1sr  10492  m1r  10493  addclsr  10494  mulclsr  10495  quseccl  18327  orbsta  18434  frgpeccl  18878  qustgphaus  22726  vitalilem2  24211  vitalilem3  24212  qsidomlem1  31007  pstmfval  31213
  Copyright terms: Public domain W3C validator