ereq1 - Metamath Proof Explorer

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

Theorem ereq1 7794

Description: Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)

**Assertion**
Ref	Expression
ereq1	⊢ (𝑅 = 𝑆 → (𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴))

**Proof of Theorem ereq1**
Step	Hyp	Ref	Expression
1		releq 5235	. . 3 ⊢ (𝑅 = 𝑆 → (Rel 𝑅 ↔ Rel 𝑆))
2		dmeq 5356	. . . 4 ⊢ (𝑅 = 𝑆 → dom 𝑅 = dom 𝑆)
3	2	eqeq1d 2653	. . 3 ⊢ (𝑅 = 𝑆 → (dom 𝑅 = 𝐴 ↔ dom 𝑆 = 𝐴))
4		cnveq 5328	. . . . . 6 ⊢ (𝑅 = 𝑆 → ^◡𝑅 = ^◡𝑆)
5		coeq1 5312	. . . . . . 7 ⊢ (𝑅 = 𝑆 → (𝑅 ∘ 𝑅) = (𝑆 ∘ 𝑅))
6		coeq2 5313	. . . . . . 7 ⊢ (𝑅 = 𝑆 → (𝑆 ∘ 𝑅) = (𝑆 ∘ 𝑆))
7	5, 6	eqtrd 2685	. . . . . 6 ⊢ (𝑅 = 𝑆 → (𝑅 ∘ 𝑅) = (𝑆 ∘ 𝑆))
8	4, 7	uneq12d 3801	. . . . 5 ⊢ (𝑅 = 𝑆 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) = (^◡𝑆 ∪ (𝑆 ∘ 𝑆)))
9	8	sseq1d 3665	. . . 4 ⊢ (𝑅 = 𝑆 → ((^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑅))
10		sseq2 3660	. . . 4 ⊢ (𝑅 = 𝑆 → ((^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆))
11	9, 10	bitrd 268	. . 3 ⊢ (𝑅 = 𝑆 → ((^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆))
12	1, 3, 11	3anbi123d 1439	. 2 ⊢ (𝑅 = 𝑆 → ((Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅) ↔ (Rel 𝑆 ∧ dom 𝑆 = 𝐴 ∧ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆)))
13		df-er 7787	. 2 ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
14		df-er 7787	. 2 ⊢ (𝑆 Er 𝐴 ↔ (Rel 𝑆 ∧ dom 𝑆 = 𝐴 ∧ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆))
15	12, 13, 14	3bitr4g 303	1 ⊢ (𝑅 = 𝑆 → (𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ w3a 1054 = wceq 1523 ∪ cun 3605 ⊆ wss 3607 ^◡ccnv 5142 dom cdm 5143 ∘ ccom 5147 Rel wrel 5148 Er wer 7784

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-opab 4746 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-er 7787

This theorem is referenced by: riiner 7863 efglem 18175 efger 18177 efgrelexlemb 18209 efgcpbllemb 18214 frgpuplem 18231 qtophaus 30031 pstmxmet 30068

W3C validator