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 8660

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 8657	. . . . . 6 ⊢ (𝑅 Er 𝑋 → Rel 𝑅)
4	2, 3	syl 17	. . . . 5 ⊢ (𝜑 → Rel 𝑅)
5		brrelex12 5683	. . . . 5 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
6	4, 1, 5	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
7		brcnvg 5833	. . . . 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 8648	. . . . . 6 ⊢ (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
12	11	simp3bi 1147	. . . . 5 ⊢ (𝑅 Er 𝑋 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)
13	2, 12	syl 17	. . . 4 ⊢ (𝜑 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)
14	13	unssad 4152	. . 3 ⊢ (𝜑 → ^◡𝑅 ⊆ 𝑅)
15	14	ssbrd 5145	. 2 ⊢ (𝜑 → (𝐵^◡𝑅𝐴 → 𝐵𝑅𝐴))
16	10, 15	mpd 15	1 ⊢ (𝜑 → 𝐵𝑅𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 Vcvv 3444 ∪ cun 3909 ⊆ wss 3911 class class class wbr 5102 ^◡ccnv 5630 dom cdm 5631 ∘ ccom 5635 Rel wrel 5636 Er wer 8645

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pr 5382

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-ral 3045 df-rex 3054 df-rab 3403 df-v 3446 df-dif 3914 df-un 3916 df-ss 3928 df-nul 4293 df-if 4485 df-sn 4586 df-pr 4588 df-op 4592 df-br 5103 df-opab 5165 df-xp 5637 df-rel 5638 df-cnv 5639 df-er 8648

This theorem is referenced by: ercl2 8661 ersymb 8662 ertr2d 8665 ertr3d 8666 ertr4d 8667 erth 8702 erinxp 8741 nqereu 10858 nqerf 10859 1nqenq 10891 qusgrp2 18966 efginvrel2 19633 efgcpbllemb 19661 2idlcpblrng 21157 tgptsmscls 24013 nsgqusf1olem3 33359 qsnzr 33399 qsalrel 42201 prjspner01 42586

W3C validator