Theorem erth 8755

Description: Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)

Hypotheses

Ref	Expression
erth.1	⊢ (𝜑 → 𝑅 Er 𝑋)
erth.2	⊢ (𝜑 → 𝐴 ∈ 𝑋)

Assertion

Ref	Expression
erth	⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))

Proof of Theorem erth

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		erth.1	. . . . . . . 8 ⊢ (𝜑 → 𝑅 Er 𝑋)
2	1	ersymb 8715	. . . . . . 7 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴))
3	2	biimpa 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → 𝐵𝑅𝐴)
4	1	ertr 8716	. . . . . . 7 ⊢ (𝜑 → ((𝐵𝑅𝐴 ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥))
5	4	impl 461	. . . . . 6 ⊢ (((𝜑 ∧ 𝐵𝑅𝐴) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
6	3, 5	syldanl 614	. . . . 5 ⊢ (((𝜑 ∧ 𝐴𝑅𝐵) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
7	1	ertr 8716	. . . . . 6 ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝑥) → 𝐴𝑅𝑥))
8	7	impl 461	. . . . 5 ⊢ (((𝜑 ∧ 𝐴𝑅𝐵) ∧ 𝐵𝑅𝑥) → 𝐴𝑅𝑥)
9	6, 8	impbida 813	. . . 4 ⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝐴𝑅𝑥 ↔ 𝐵𝑅𝑥))
10		vex 3461	. . . . 5 ⊢ 𝑥 ∈ V
11		erth.2	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
12	11	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ 𝑋)
13		elecg 8745	. . . . 5 ⊢ ((𝑥 ∈ V ∧ 𝐴 ∈ 𝑋) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥))
14	10, 12, 13	sylancr 599	. . . 4 ⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝑥))
15		errel 8710	. . . . . . 7 ⊢ (𝑅 Er 𝑋 → Rel 𝑅)
16	1, 15	syl 18	. . . . . 6 ⊢ (𝜑 → Rel 𝑅)
17		brrelex2 5717	. . . . . 6 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
18	16, 17	sylan 592	. . . . 5 ⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)
19		elecg 8745	. . . . 5 ⊢ ((𝑥 ∈ V ∧ 𝐵 ∈ V) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥))
20	10, 18, 19	sylancr 599	. . . 4 ⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝑥 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝑥))
21	9, 14, 20	3bitr4d 314	. . 3 ⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅 ↔ 𝑥 ∈ [𝐵]𝑅))
22	21	eqrdv 2763	. 2 ⊢ ((𝜑 ∧ 𝐴𝑅𝐵) → [𝐴]𝑅 = [𝐵]𝑅)
23	1	adantr 486	. . 3 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝑅 Er 𝑋)
24	1, 11	erref 8721	. . . . . . 7 ⊢ (𝜑 → 𝐴𝑅𝐴)
25	24	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐴)
26	11	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ 𝑋)
27		elecg 8745	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐴))
28	26, 26, 27	syl2anc 596	. . . . . 6 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐴]𝑅 ↔ 𝐴𝑅𝐴))
29	25, 28	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐴]𝑅)
30		simpr 490	. . . . 5 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)
31	29, 30	eleqtrd 2867	. . . 4 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐵]𝑅)
32	23, 30	ereldm 8754	. . . . . 6 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋))
33	26, 32	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵 ∈ 𝑋)
34		elecg 8745	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
35	26, 33, 34	syl2anc 596	. . . 4 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
36	31, 35	mpbid 235	. . 3 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑅𝐴)
37	23, 36	ersym 8713	. 2 ⊢ ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐵)
38	22, 37	impbida 813	1 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Vcvv 3457   class class class wbr 5111  Rel wrel 5668   Er wer 8697  [cec 8698

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-er 8700  df-ec 8702

This theorem is used by:  erth2  8756  erthi  8757  qliftfun  8806  eroveu  8816  eceqoveq  8826  enreceq  11070  prsrlem1  11076  ercpbllem  17628  eqg0el  19302  orbsta  19431  sylow2blem3  19740  qusecsub  19953  frgpnabllem2  19992  rngqipring1  21510  qsnzr  21537  zndvds  21753  qustgpopn  24332  qustgphaus  24335  pi1xfrf  25267  pi1cof  25273  tgjustr  28798  erld2  33654  rlocf1  33662  fracfld  33697  qusvscpbl  33739  nsgqusf1olem3  33792  zringfrac  33912  pstmxmet  34355  sconnpi1  35772  topfneec2  36928