Theorem erthi 8758

Description: Basic property of equivalence relations. Part of Lemma 3N of [Enderton] p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)

Hypotheses

Ref	Expression
erthi.1	⊢ (𝜑 → 𝑅 Er 𝑋)
erthi.2	⊢ (𝜑 → 𝐴𝑅𝐵)

Assertion

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

Proof of Theorem erthi

Step	Hyp	Ref	Expression
1		erthi.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		erthi.1	. . 3 ⊢ (𝜑 → 𝑅 Er 𝑋)
3	2, 1	ercl 8713	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
4	2, 3	erth 8756	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
5	1, 4	mpbid 235	1 ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5103   Er wer 8698  [cec 8699

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-er 8701  df-ec 8703

This theorem is used by:  erdisj  8759  qsel  8801  addsrmo  11139  mulsrmo  11140  qusmgm  18844  qusmnd  18955  qusgrp2  19248  frgpinv  19958  qustgpopn  24419  blpnfctr  24735  pi1inv  25353  pi1xfrf  25354  pi1xfr  25356  pi1xfrcnvlem  25357  pi1cof  25360  vitalilem3  25911  rloccring  33814  rlocinvunit  33818  rlocisunit  33819  fracfld  33852  qsdrngilem  34000  zringfrac  34068  sconnpi1  35973  qsalrel  43260