Theorem elecg 8766

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

Step	Hyp	Ref	Expression
1		elimasng 6086	. . 3 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ (𝑅 “ {𝐵}) ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
2	1	ancoms 464	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝑅 “ {𝐵}) ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
3		df-ec 8723	. . 3 ⊢ [𝐵]𝑅 = (𝑅 “ {𝐵})
4	3	eleq2i 2852	. 2 ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐴 ∈ (𝑅 “ {𝐵}))
5		df-br 5103	. 2 ⊢ (𝐵𝑅𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
6	2, 4, 5	3bitr4g 317	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  {csn 4584  ⟨cop 4834   class class class wbr 5102   “ cima 5653  [cec 8719

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-ec 8723

This theorem is used by:  ecref  8767  elec  8768  relelec  8769  ecdmn0  8774  erth  8776  erdisj  8779  qsel  8821  ecxpid  19392  ghmqusnsglem1  19500  ghmquskerlem1  19503  orbsta  19533  sylow2alem1  19837  sylow2blem1  19840  sylow3lem3  19849  efgi2  19945  rngqiprngfulem2  21614  rngqipring1  21618  tgpconncompeqg  24437  xmetec  24759  blpnfctr  24761  xmetresbl  24762  xrsblre  25137  lsmsnorb  33993  ecin0  39378  eqvrelth  39721  qsalrel  43386