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 8530

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 8527	. . . . . 6 ⊢ (𝑅 Er 𝑋 → Rel 𝑅)
4	2, 3	syl 17	. . . . 5 ⊢ (𝜑 → Rel 𝑅)
5		brrelex12 5641	. . . . 5 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
6	4, 1, 5	syl2anc 583	. . . 4 ⊢ (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
7		brcnvg 5792	. . . . 5 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝐵^◡𝑅𝐴 ↔ 𝐴𝑅𝐵))
8	7	ancoms 458	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐵^◡𝑅𝐴 ↔ 𝐴𝑅𝐵))
9	6, 8	syl 17	. . 3 ⊢ (𝜑 → (𝐵^◡𝑅𝐴 ↔ 𝐴𝑅𝐵))
10	1, 9	mpbird 256	. 2 ⊢ (𝜑 → 𝐵^◡𝑅𝐴)
11		df-er 8518	. . . . . 6 ⊢ (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
12	11	simp3bi 1145	. . . . 5 ⊢ (𝑅 Er 𝑋 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)
13	2, 12	syl 17	. . . 4 ⊢ (𝜑 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)
14	13	unssad 4124	. . 3 ⊢ (𝜑 → ^◡𝑅 ⊆ 𝑅)
15	14	ssbrd 5120	. 2 ⊢ (𝜑 → (𝐵^◡𝑅𝐴 → 𝐵𝑅𝐴))
16	10, 15	mpd 15	1 ⊢ (𝜑 → 𝐵𝑅𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1537 ∈ wcel 2101 Vcvv 3434 ∪ cun 3887 ⊆ wss 3889 class class class wbr 5077 ^◡ccnv 5590 dom cdm 5591 ∘ ccom 5595 Rel wrel 5596 Er wer 8515

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-ext 2704 ax-sep 5226 ax-nul 5233 ax-pr 5355

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-sb 2063 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3060 df-rex 3069 df-rab 3224 df-v 3436 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4260 df-if 4463 df-sn 4565 df-pr 4567 df-op 4571 df-br 5078 df-opab 5140 df-xp 5597 df-rel 5598 df-cnv 5599 df-er 8518

This theorem is referenced by: ercl2 8531 ersymb 8532 ertr2d 8535 ertr3d 8536 ertr4d 8537 erth 8567 erinxp 8600 nqereu 10713 nqerf 10714 1nqenq 10746 qusgrp2 18721 efginvrel2 19361 efgcpbllemb 19389 2idlcpbl 20533 tgptsmscls 23329 nsgqusf1olem3 31628 qsalrel 40238 prjspner01 40485

W3C validator