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

Theorem elec 8626
Description: Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.)
Hypotheses
Ref Expression
elec.1 𝐴 ∈ V
elec.2 𝐵 ∈ V
Assertion
Ref Expression
elec (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴)

Proof of Theorem elec
StepHypRef Expression
1 elec.1 . 2 𝐴 ∈ V
2 elec.2 . 2 𝐵 ∈ V
3 elecg 8625 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
41, 2, 3mp2an 691 1 (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wcel 2107  Vcvv 3444   class class class wbr 5104  [cec 8580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ec 8584
This theorem is referenced by:  ecid  8655  sylow2alem2  19330  sylow2a  19331  sylow2blem1  19332  efgval2  19436  efgrelexlemb  19462  efgcpbllemb  19467  frgpnabllem1  19581  tgpconncomp  23387  qustgphaus  23397  vitalilem2  24896  vitalilem3  24897  isbndx  36137  prtlem10  37223  prtlem19  37236  prter3  37240
  Copyright terms: Public domain W3C validator