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

Theorem ersym 8158
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
StepHypRef Expression
1 ersym.2 . . 3 (𝜑𝐴𝑅𝐵)
2 ersym.1 . . . . . 6 (𝜑𝑅 Er 𝑋)
3 errel 8155 . . . . . 6 (𝑅 Er 𝑋 → Rel 𝑅)
42, 3syl 17 . . . . 5 (𝜑 → Rel 𝑅)
5 brrelex12 5497 . . . . 5 ((Rel 𝑅𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
64, 1, 5syl2anc 584 . . . 4 (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
7 brcnvg 5643 . . . . 5 ((𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝐵𝑅𝐴𝐴𝑅𝐵))
87ancoms 459 . . . 4 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐵𝑅𝐴𝐴𝑅𝐵))
96, 8syl 17 . . 3 (𝜑 → (𝐵𝑅𝐴𝐴𝑅𝐵))
101, 9mpbird 258 . 2 (𝜑𝐵𝑅𝐴)
11 df-er 8146 . . . . . 6 (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
1211simp3bi 1140 . . . . 5 (𝑅 Er 𝑋 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
132, 12syl 17 . . . 4 (𝜑 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
1413unssad 4090 . . 3 (𝜑𝑅𝑅)
1514ssbrd 5011 . 2 (𝜑 → (𝐵𝑅𝐴𝐵𝑅𝐴))
1610, 15mpd 15 1 (𝜑𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1525  wcel 2083  Vcvv 3440  cun 3863  wss 3865   class class class wbr 4968  ccnv 5449  dom cdm 5450  ccom 5454  Rel wrel 5455   Er wer 8143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-br 4969  df-opab 5031  df-xp 5456  df-rel 5457  df-cnv 5458  df-er 8146
This theorem is referenced by:  ercl2  8159  ersymb  8160  ertr2d  8163  ertr3d  8164  ertr4d  8165  erth  8195  erinxp  8228  nqereu  10204  nqerf  10205  1nqenq  10237  qusgrp2  17978  efginvrel2  18584  efgcpbllemb  18612  2idlcpbl  19700  tgptsmscls  22445  qsalrel  38676
  Copyright terms: Public domain W3C validator