ersym - Metamath Proof Explorer

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

Theorem ersym 8645

Description: An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)

**Hypotheses**
Ref	Expression
ersym.1	⊢ (𝜑 → 𝑅 Er 𝑋)
ersym.2	⊢ (𝜑 → 𝐴𝑅𝐵)

**Assertion**
Ref	Expression
ersym	⊢ (𝜑 → 𝐵𝑅𝐴)

**Proof of Theorem ersym**
Step	Hyp	Ref	Expression
1		ersym.2	. . 3 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		ersym.1	. . . . . 6 ⊢ (𝜑 → 𝑅 Er 𝑋)
3		errel 8642	. . . . . 6 ⊢ (𝑅 Er 𝑋 → Rel 𝑅)
4	2, 3	syl 17	. . . . 5 ⊢ (𝜑 → Rel 𝑅)
5		brrelex12 5674	. . . . 5 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
6	4, 1, 5	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
7		brcnvg 5826	. . . . 5 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝐵^◡𝑅𝐴 ↔ 𝐴𝑅𝐵))
8	7	ancoms 458	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐵^◡𝑅𝐴 ↔ 𝐴𝑅𝐵))
9	6, 8	syl 17	. . 3 ⊢ (𝜑 → (𝐵^◡𝑅𝐴 ↔ 𝐴𝑅𝐵))
10	1, 9	mpbird 257	. 2 ⊢ (𝜑 → 𝐵^◡𝑅𝐴)
11		df-er 8633	. . . . . 6 ⊢ (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
12	11	simp3bi 1147	. . . . 5 ⊢ (𝑅 Er 𝑋 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)
13	2, 12	syl 17	. . . 4 ⊢ (𝜑 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)
14	13	unssad 4143	. . 3 ⊢ (𝜑 → ^◡𝑅 ⊆ 𝑅)
15	14	ssbrd 5139	. 2 ⊢ (𝜑 → (𝐵^◡𝑅𝐴 → 𝐵𝑅𝐴))
16	10, 15	mpd 15	1 ⊢ (𝜑 → 𝐵𝑅𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2113 Vcvv 3438 ∪ cun 3897 ⊆ wss 3899 class class class wbr 5096 ^◡ccnv 5621 dom cdm 5622 ∘ ccom 5626 Rel wrel 5627 Er wer 8630

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 2706 ax-sep 5239 ax-nul 5249 ax-pr 5375

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 2713 df-cleq 2726 df-clel 2809 df-ral 3050 df-rex 3059 df-rab 3398 df-v 3440 df-dif 3902 df-un 3904 df-ss 3916 df-nul 4284 df-if 4478 df-sn 4579 df-pr 4581 df-op 4585 df-br 5097 df-opab 5159 df-xp 5628 df-rel 5629 df-cnv 5630 df-er 8633

This theorem is referenced by: ercl2 8646 ersymb 8647 ertr2d 8650 ertr3d 8651 ertr4d 8652 erth 8687 erinxp 8726 nqereu 10838 nqerf 10839 1nqenq 10871 qusgrp2 18986 efginvrel2 19654 efgcpbllemb 19682 2idlcpblrng 21224 tgptsmscls 24092 nsgqusf1olem3 33445 qsnzr 33485 qsalrel 42438 prjspner01 42810 chnerlem1 47068 chner 47071

W3C validator