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

Theorem ersym 8756
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 8753 . . . . . 6 (𝑅 Er 𝑋 → Rel 𝑅)
42, 3syl 17 . . . . 5 (𝜑 → Rel 𝑅)
5 brrelex12 5741 . . . . 5 ((Rel 𝑅𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
64, 1, 5syl2anc 584 . . . 4 (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
7 brcnvg 5893 . . . . 5 ((𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝐵𝑅𝐴𝐴𝑅𝐵))
87ancoms 458 . . . 4 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐵𝑅𝐴𝐴𝑅𝐵))
96, 8syl 17 . . 3 (𝜑 → (𝐵𝑅𝐴𝐴𝑅𝐵))
101, 9mpbird 257 . 2 (𝜑𝐵𝑅𝐴)
11 df-er 8744 . . . . . 6 (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
1211simp3bi 1146 . . . . 5 (𝑅 Er 𝑋 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
132, 12syl 17 . . . 4 (𝜑 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
1413unssad 4203 . . 3 (𝜑𝑅𝑅)
1514ssbrd 5191 . 2 (𝜑 → (𝐵𝑅𝐴𝐵𝑅𝐴))
1610, 15mpd 15 1 (𝜑𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  Vcvv 3478  cun 3961  wss 3963   class class class wbr 5148  ccnv 5688  dom cdm 5689  ccom 5693  Rel wrel 5694   Er wer 8741
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-cnv 5697  df-er 8744
This theorem is referenced by:  ercl2  8757  ersymb  8758  ertr2d  8761  ertr3d  8762  ertr4d  8763  erth  8795  erinxp  8830  nqereu  10967  nqerf  10968  1nqenq  11000  qusgrp2  19089  efginvrel2  19760  efgcpbllemb  19788  2idlcpblrng  21299  tgptsmscls  24174  nsgqusf1olem3  33423  qsnzr  33463  qsalrel  42260  prjspner01  42612
  Copyright terms: Public domain W3C validator