ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ersym GIF version

Theorem ersym 6407
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 6404 . . . . . 6 (𝑅 Er 𝑋 → Rel 𝑅)
42, 3syl 14 . . . . 5 (𝜑 → Rel 𝑅)
5 brrelex12 4545 . . . . 5 ((Rel 𝑅𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
64, 1, 5syl2anc 406 . . . 4 (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
7 brcnvg 4688 . . . . 5 ((𝐵 ∈ V ∧ 𝐴 ∈ V) → (𝐵𝑅𝐴𝐴𝑅𝐵))
87ancoms 266 . . . 4 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐵𝑅𝐴𝐴𝑅𝐵))
96, 8syl 14 . . 3 (𝜑 → (𝐵𝑅𝐴𝐴𝑅𝐵))
101, 9mpbird 166 . 2 (𝜑𝐵𝑅𝐴)
11 df-er 6395 . . . . . 6 (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
1211simp3bi 981 . . . . 5 (𝑅 Er 𝑋 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
132, 12syl 14 . . . 4 (𝜑 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
1413unssad 3221 . . 3 (𝜑𝑅𝑅)
1514ssbrd 3939 . 2 (𝜑 → (𝐵𝑅𝐴𝐵𝑅𝐴))
1610, 15mpd 13 1 (𝜑𝐵𝑅𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1314  wcel 1463  Vcvv 2658  cun 3037  wss 3039   class class class wbr 3897  ccnv 4506  dom cdm 4507  ccom 4511  Rel wrel 4512   Er wer 6392
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-v 2660  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-br 3898  df-opab 3958  df-xp 4513  df-rel 4514  df-cnv 4515  df-er 6395
This theorem is referenced by:  ercl2  6408  ersymb  6409  ertr2d  6412  ertr3d  6413  ertr4d  6414  erth  6439  erinxp  6469
  Copyright terms: Public domain W3C validator