Theorem elecg 8541

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 5996	. . 3 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ (𝑅 “ {𝐵}) ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
2	1	ancoms 459	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝑅 “ {𝐵}) ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
3		df-ec 8500	. . 3 ⊢ [𝐵]𝑅 = (𝑅 “ {𝐵})
4	3	eleq2i 2830	. 2 ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐴 ∈ (𝑅 “ {𝐵}))
5		df-br 5075	. 2 ⊢ (𝐵𝑅𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
6	2, 4, 5	3bitr4g 314	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  {csn 4561  ⟨cop 4567   class class class wbr 5074   “ cima 5592  [cec 8496

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ec 8500

This theorem is referenced by:  elec  8542  relelec  8543  ecdmn0  8545  erth  8547  erdisj  8550  qsel  8585  orbsta  18919  sylow2alem1  19222  sylow2blem1  19225  sylow3lem3  19234  efgi2  19331  tgpconncompeqg  23263  xmetec  23587  blpnfctr  23589  xmetresbl  23590  xrsblre  23974  ecxpid  31556  lsmsnorb  31579  ecin0  36484  eqvrelth  36724  qsalrel  40215