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 8650

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 8647	. . . . . 6 ⊢ (𝑅 Er 𝑋 → Rel 𝑅)
4	2, 3	syl 17	. . . . 5 ⊢ (𝜑 → Rel 𝑅)
5		brrelex12 5677	. . . . 5 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
6	4, 1, 5	syl2anc 585	. . . 4 ⊢ (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
7		brcnvg 5829	. . . . 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 8637	. . . . . 6 ⊢ (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
12	11	simp3bi 1148	. . . . 5 ⊢ (𝑅 Er 𝑋 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)
13	2, 12	syl 17	. . . 4 ⊢ (𝜑 → (^◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)
14	13	unssad 4146	. . 3 ⊢ (𝜑 → ^◡𝑅 ⊆ 𝑅)
15	14	ssbrd 5142	. 2 ⊢ (𝜑 → (𝐵^◡𝑅𝐴 → 𝐵𝑅𝐴))
16	10, 15	mpd 15	1 ⊢ (𝜑 → 𝐵𝑅𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 Vcvv 3441 ∪ cun 3900 ⊆ wss 3902 class class class wbr 5099 ^◡ccnv 5624 dom cdm 5625 ∘ ccom 5629 Rel wrel 5630 Er wer 8634

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-sep 5242 ax-nul 5252 ax-pr 5378

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-ral 3053 df-rex 3062 df-rab 3401 df-v 3443 df-dif 3905 df-un 3907 df-ss 3919 df-nul 4287 df-if 4481 df-sn 4582 df-pr 4584 df-op 4588 df-br 5100 df-opab 5162 df-xp 5631 df-rel 5632 df-cnv 5633 df-er 8637

This theorem is referenced by: ercl2 8651 ersymb 8652 ertr2d 8655 ertr3d 8656 ertr4d 8657 erth 8692 erinxp 8732 nqereu 10844 nqerf 10845 1nqenq 10877 qusgrp2 18992 efginvrel2 19660 efgcpbllemb 19688 2idlcpblrng 21230 tgptsmscls 24098 nsgqusf1olem3 33477 qsnzr 33517 qsalrel 42532 prjspner01 42904 chnerlem1 47162 chner 47165

W3C validator