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

Theorem elecg 7770
Description: Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.)
Assertion
Ref Expression
elecg ((𝐴𝑉𝐵𝑊) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))

Proof of Theorem elecg
StepHypRef Expression
1 elimasng 5479 . . 3 ((𝐵𝑊𝐴𝑉) → (𝐴 ∈ (𝑅 “ {𝐵}) ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
21ancoms 469 . 2 ((𝐴𝑉𝐵𝑊) → (𝐴 ∈ (𝑅 “ {𝐵}) ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
3 df-ec 7729 . . 3 [𝐵]𝑅 = (𝑅 “ {𝐵})
43eleq2i 2691 . 2 (𝐴 ∈ [𝐵]𝑅𝐴 ∈ (𝑅 “ {𝐵}))
5 df-br 4645 . 2 (𝐵𝑅𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
62, 4, 53bitr4g 303 1 ((𝐴𝑉𝐵𝑊) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wcel 1988  {csn 4168  cop 4174   class class class wbr 4644  cima 5107  [cec 7725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-xp 5110  df-cnv 5112  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-ec 7729
This theorem is referenced by:  elec  7771  relelec  7772  ecdmn0  7774  erth  7776  erdisj  7779  qsel  7811  orbsta  17727  sylow2alem1  18013  sylow2blem1  18016  sylow3lem3  18025  efgi2  18119  tgpconncompeqg  21896  xmetec  22220  blpnfctr  22222  xmetresbl  22223  xrsblre  22595
  Copyright terms: Public domain W3C validator