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 8638

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 5723	. . 3 ⊢ (𝑅 = 𝑆 → (Rel 𝑅 ↔ Rel 𝑆))
2		dmeq 5849	. . . 4 ⊢ (𝑅 = 𝑆 → dom 𝑅 = dom 𝑆)
3	2	eqeq1d 2735	. . 3 ⊢ (𝑅 = 𝑆 → (dom 𝑅 = 𝐴 ↔ dom 𝑆 = 𝐴))
4		cnveq 5819	. . . . . 6 ⊢ (𝑅 = 𝑆 → ^◡𝑅 = ^◡𝑆)
5		coeq1 5803	. . . . . . 7 ⊢ (𝑅 = 𝑆 → (𝑅 ∘ 𝑅) = (𝑆 ∘ 𝑅))
6		coeq2 5804	. . . . . . 7 ⊢ (𝑅 = 𝑆 → (𝑆 ∘ 𝑅) = (𝑆 ∘ 𝑆))
7	5, 6	eqtrd 2768	. . . . . 6 ⊢ (𝑅 = 𝑆 → (𝑅 ∘ 𝑅) = (𝑆 ∘ 𝑆))
8	4, 7	uneq12d 4118	. . . . 5 ⊢ (𝑅 = 𝑆 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) = (^◡𝑆 ∪ (𝑆 ∘ 𝑆)))
9	8	sseq1d 3962	. . . 4 ⊢ (𝑅 = 𝑆 → ((^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑅))
10		sseq2 3957	. . . 4 ⊢ (𝑅 = 𝑆 → ((^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆))
11	9, 10	bitrd 279	. . 3 ⊢ (𝑅 = 𝑆 → ((^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆))
12	1, 3, 11	3anbi123d 1438	. 2 ⊢ (𝑅 = 𝑆 → ((Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅) ↔ (Rel 𝑆 ∧ dom 𝑆 = 𝐴 ∧ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆)))
13		df-er 8631	. 2 ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
14		df-er 8631	. 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 1086 = wceq 1541 ∪ cun 3896 ⊆ wss 3898 ^◡ccnv 5620 dom cdm 5621 ∘ ccom 5625 Rel wrel 5626 Er wer 8628

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2705

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2712 df-cleq 2725 df-clel 2808 df-rab 3397 df-v 3439 df-dif 3901 df-un 3903 df-ss 3915 df-nul 4283 df-if 4477 df-sn 4578 df-pr 4580 df-op 4584 df-br 5096 df-opab 5158 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-er 8631

This theorem is referenced by: riiner 8723 efglem 19636 efger 19638 efgrelexlemb 19670 efgcpbllemb 19675 frgpuplem 19692 tgjustf 28471 qtophaus 33921 pstmxmet 33982 prjspner 42777

W3C validator