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

Theorem ersym 8721
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 8718 . . . . . 6 (𝑅 Er 𝑋 → Rel 𝑅)
42, 3syl 17 . . . . 5 (𝜑 → Rel 𝑅)
5 brrelex12 5728 . . . . 5 ((Rel 𝑅𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
64, 1, 5syl2anc 583 . . . 4 (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
7 brcnvg 5879 . . . . 5 ((𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝐵𝑅𝐴𝐴𝑅𝐵))
87ancoms 458 . . . 4 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐵𝑅𝐴𝐴𝑅𝐵))
96, 8syl 17 . . 3 (𝜑 → (𝐵𝑅𝐴𝐴𝑅𝐵))
101, 9mpbird 257 . 2 (𝜑𝐵𝑅𝐴)
11 df-er 8709 . . . . . 6 (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
1211simp3bi 1146 . . . . 5 (𝑅 Er 𝑋 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
132, 12syl 17 . . . 4 (𝜑 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
1413unssad 4187 . . 3 (𝜑𝑅𝑅)
1514ssbrd 5191 . 2 (𝜑 → (𝐵𝑅𝐴𝐵𝑅𝐴))
1610, 15mpd 15 1 (𝜑𝐵𝑅𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1540  wcel 2105  Vcvv 3473  cun 3946  wss 3948   class class class wbr 5148  ccnv 5675  dom cdm 5676  ccom 5680  Rel wrel 5681   Er wer 8706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-cnv 5684  df-er 8709
This theorem is referenced by:  ercl2  8722  ersymb  8723  ertr2d  8726  ertr3d  8727  ertr4d  8728  erth  8758  erinxp  8791  nqereu  10930  nqerf  10931  1nqenq  10963  qusgrp2  18984  efginvrel2  19643  efgcpbllemb  19671  2idlcpblrng  21109  tgptsmscls  23974  nsgqusf1olem3  32966  qsnzr  33014  qsalrel  41529  prjspner01  41830
  Copyright terms: Public domain W3C validator