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 8683

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 8680	. . . . . 6 ⊢ (𝑅 Er 𝑋 → Rel 𝑅)
4	2, 3	syl 17	. . . . 5 ⊢ (𝜑 → Rel 𝑅)
5		brrelex12 5690	. . . . 5 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
6	4, 1, 5	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
7		brcnvg 5843	. . . . 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 8671	. . . . . 6 ⊢ (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
12	11	simp3bi 1147	. . . . 5 ⊢ (𝑅 Er 𝑋 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)
13	2, 12	syl 17	. . . 4 ⊢ (𝜑 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)
14	13	unssad 4156	. . 3 ⊢ (𝜑 → ^◡𝑅 ⊆ 𝑅)
15	14	ssbrd 5150	. 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 3447 ∪ cun 3912 ⊆ wss 3914 class class class wbr 5107 ^◡ccnv 5637 dom cdm 5638 ∘ ccom 5642 Rel wrel 5643 Er wer 8668

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 5251 ax-nul 5261 ax-pr 5387

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 3406 df-v 3449 df-dif 3917 df-un 3919 df-ss 3931 df-nul 4297 df-if 4489 df-sn 4590 df-pr 4592 df-op 4596 df-br 5108 df-opab 5170 df-xp 5644 df-rel 5645 df-cnv 5646 df-er 8671

This theorem is referenced by: ercl2 8684 ersymb 8685 ertr2d 8688 ertr3d 8689 ertr4d 8690 erth 8725 erinxp 8764 nqereu 10882 nqerf 10883 1nqenq 10915 qusgrp2 18990 efginvrel2 19657 efgcpbllemb 19685 2idlcpblrng 21181 tgptsmscls 24037 nsgqusf1olem3 33386 qsnzr 33426 qsalrel 42228 prjspner01 42613

W3C validator