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

Theorem cnvsym 6134
Description: Two ways of saying a relation is symmetric. Similar to definition of symmetry in [Schechter] p. 51. (Contributed by NM, 28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by SN, 23-Dec-2024.) Avoid ax-11 2154. (Revised by BTernaryTau, 29-Dec-2024.)
Assertion
Ref Expression
cnvsym (𝑅𝑅 ↔ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥))
Distinct variable group:   𝑥,𝑦,𝑅

Proof of Theorem cnvsym
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 relcnv 6124 . . 3 Rel 𝑅
2 ssrel3 5798 . . 3 (Rel 𝑅 → (𝑅𝑅 ↔ ∀𝑦𝑥(𝑦𝑅𝑥𝑦𝑅𝑥)))
31, 2ax-mp 5 . 2 (𝑅𝑅 ↔ ∀𝑦𝑥(𝑦𝑅𝑥𝑦𝑅𝑥))
4 breq1 5150 . . . 4 (𝑦 = 𝑧 → (𝑦𝑅𝑥𝑧𝑅𝑥))
5 breq1 5150 . . . 4 (𝑦 = 𝑧 → (𝑦𝑅𝑥𝑧𝑅𝑥))
64, 5imbi12d 344 . . 3 (𝑦 = 𝑧 → ((𝑦𝑅𝑥𝑦𝑅𝑥) ↔ (𝑧𝑅𝑥𝑧𝑅𝑥)))
7 breq2 5151 . . . 4 (𝑥 = 𝑧 → (𝑦𝑅𝑥𝑦𝑅𝑧))
8 breq2 5151 . . . 4 (𝑥 = 𝑧 → (𝑦𝑅𝑥𝑦𝑅𝑧))
97, 8imbi12d 344 . . 3 (𝑥 = 𝑧 → ((𝑦𝑅𝑥𝑦𝑅𝑥) ↔ (𝑦𝑅𝑧𝑦𝑅𝑧)))
106, 9alcomw 2041 . 2 (∀𝑦𝑥(𝑦𝑅𝑥𝑦𝑅𝑥) ↔ ∀𝑥𝑦(𝑦𝑅𝑥𝑦𝑅𝑥))
11 vex 3481 . . . . 5 𝑦 ∈ V
12 vex 3481 . . . . 5 𝑥 ∈ V
1311, 12brcnv 5895 . . . 4 (𝑦𝑅𝑥𝑥𝑅𝑦)
1413imbi1i 349 . . 3 ((𝑦𝑅𝑥𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦𝑦𝑅𝑥))
15142albii 1816 . 2 (∀𝑥𝑦(𝑦𝑅𝑥𝑦𝑅𝑥) ↔ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥))
163, 10, 153bitri 297 1 (𝑅𝑅 ↔ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1534  wss 3962   class class class wbr 5147  ccnv 5687  Rel wrel 5693
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-cnv 5696
This theorem is referenced by:  dfer2  8744  relcnveq3  38302  relcnveq  38303  relcnveq2  38304  cnvcosseq  38418  symrelcoss2  38447  elrelscnveq3  38472  elrelscnveq  38473  elrelscnveq2  38474  dfsymrels3  38527  dfsymrel3  38531  symrefref3  38545  refsymrels3  38547  elrefsymrels3  38551  dfeqvrels3  38570
  Copyright terms: Public domain W3C validator