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 8298

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 5653	. . 3 ⊢ (𝑅 = 𝑆 → (Rel 𝑅 ↔ Rel 𝑆))
2		dmeq 5774	. . . 4 ⊢ (𝑅 = 𝑆 → dom 𝑅 = dom 𝑆)
3	2	eqeq1d 2825	. . 3 ⊢ (𝑅 = 𝑆 → (dom 𝑅 = 𝐴 ↔ dom 𝑆 = 𝐴))
4		cnveq 5746	. . . . . 6 ⊢ (𝑅 = 𝑆 → ^◡𝑅 = ^◡𝑆)
5		coeq1 5730	. . . . . . 7 ⊢ (𝑅 = 𝑆 → (𝑅 ∘ 𝑅) = (𝑆 ∘ 𝑅))
6		coeq2 5731	. . . . . . 7 ⊢ (𝑅 = 𝑆 → (𝑆 ∘ 𝑅) = (𝑆 ∘ 𝑆))
7	5, 6	eqtrd 2858	. . . . . 6 ⊢ (𝑅 = 𝑆 → (𝑅 ∘ 𝑅) = (𝑆 ∘ 𝑆))
8	4, 7	uneq12d 4142	. . . . 5 ⊢ (𝑅 = 𝑆 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) = (^◡𝑆 ∪ (𝑆 ∘ 𝑆)))
9	8	sseq1d 4000	. . . 4 ⊢ (𝑅 = 𝑆 → ((^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑅))
10		sseq2 3995	. . . 4 ⊢ (𝑅 = 𝑆 → ((^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆))
11	9, 10	bitrd 281	. . 3 ⊢ (𝑅 = 𝑆 → ((^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅 ↔ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆))
12	1, 3, 11	3anbi123d 1432	. 2 ⊢ (𝑅 = 𝑆 → ((Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅) ↔ (Rel 𝑆 ∧ dom 𝑆 = 𝐴 ∧ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆)))
13		df-er 8291	. 2 ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
14		df-er 8291	. 2 ⊢ (𝑆 Er 𝐴 ↔ (Rel 𝑆 ∧ dom 𝑆 = 𝐴 ∧ (^◡𝑆 ∪ (𝑆 ∘ 𝑆)) ⊆ 𝑆))
15	12, 13, 14	3bitr4g 316	1 ⊢ (𝑅 = 𝑆 → (𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ w3a 1083 = wceq 1537 ∪ cun 3936 ⊆ wss 3938 ^◡ccnv 5556 dom cdm 5557 ∘ ccom 5561 Rel wrel 5562 Er wer 8288

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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-rab 3149 df-v 3498 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-sn 4570 df-pr 4572 df-op 4576 df-br 5069 df-opab 5131 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-er 8291

This theorem is referenced by: riiner 8372 efglem 18844 efger 18846 efgrelexlemb 18878 efgcpbllemb 18883 frgpuplem 18900 tgjustf 26261 qtophaus 31102 pstmxmet 31139

W3C validator