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 8651

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 5733	. . 3 ⊢ (𝑅 = 𝑆 → (Rel 𝑅 ↔ Rel 𝑆))
2		dmeq 5858	. . . 4 ⊢ (𝑅 = 𝑆 → dom 𝑅 = dom 𝑆)
3	2	eqeq1d 2738	. . 3 ⊢ (𝑅 = 𝑆 → (dom 𝑅 = 𝐴 ↔ dom 𝑆 = 𝐴))
4		cnveq 5828	. . . . . 6 ⊢ (𝑅 = 𝑆 → ^◡𝑅 = ^◡𝑆)
5		coeq1 5812	. . . . . . 7 ⊢ (𝑅 = 𝑆 → (𝑅 ∘ 𝑅) = (𝑆 ∘ 𝑅))
6		coeq2 5813	. . . . . . 7 ⊢ (𝑅 = 𝑆 → (𝑆 ∘ 𝑅) = (𝑆 ∘ 𝑆))
7	5, 6	eqtrd 2771	. . . . . 6 ⊢ (𝑅 = 𝑆 → (𝑅 ∘ 𝑅) = (𝑆 ∘ 𝑆))
8	4, 7	uneq12d 4109	. . . . 5 ⊢ (𝑅 = 𝑆 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) = (^◡𝑆 ∪ (𝑆 ∘ 𝑆)))
9	8	sseq1d 3953	. . . 4 ⊢ (𝑅 = 𝑆 → ((^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑅))
10		sseq2 3948	. . . 4 ⊢ (𝑅 = 𝑆 → ((^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆))
11	9, 10	bitrd 279	. . 3 ⊢ (𝑅 = 𝑆 → ((^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆))
12	1, 3, 11	3anbi123d 1439	. 2 ⊢ (𝑅 = 𝑆 → ((Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅) ↔ (Rel 𝑆 ∧ dom 𝑆 = 𝐴 ∧ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆)))
13		df-er 8643	. 2 ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
14		df-er 8643	. 2 ⊢ (𝑆 Er 𝐴 ↔ (Rel 𝑆 ∧ dom 𝑆 = 𝐴 ∧ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆))
15	12, 13, 14	3bitr4g 314	1 ⊢ (𝑅 = 𝑆 → (𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ w3a 1087 = wceq 1542 ∪ cun 3887 ⊆ wss 3889 ^◡ccnv 5630 dom cdm 5631 ∘ ccom 5635 Rel wrel 5636 Er wer 8640

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2708

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2715 df-cleq 2728 df-clel 2811 df-rab 3390 df-v 3431 df-dif 3892 df-un 3894 df-ss 3906 df-nul 4274 df-if 4467 df-sn 4568 df-pr 4570 df-op 4574 df-br 5086 df-opab 5148 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-er 8643

This theorem is referenced by: riiner 8737 efglem 19691 efger 19693 efgrelexlemb 19725 efgcpbllemb 19730 frgpuplem 19747 tgjustf 28541 qtophaus 33980 pstmxmet 34041 prjspner 43052

W3C validator