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

Theorem cnvsym 6071
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 2155. (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 6061 . . 3 Rel 𝑅
2 ssrel3 5747 . . 3 (Rel 𝑅 → (𝑅𝑅 ↔ ∀𝑦𝑥(𝑦𝑅𝑥𝑦𝑅𝑥)))
31, 2ax-mp 5 . 2 (𝑅𝑅 ↔ ∀𝑦𝑥(𝑦𝑅𝑥𝑦𝑅𝑥))
4 breq1 5113 . . . 4 (𝑦 = 𝑧 → (𝑦𝑅𝑥𝑧𝑅𝑥))
5 breq1 5113 . . . 4 (𝑦 = 𝑧 → (𝑦𝑅𝑥𝑧𝑅𝑥))
64, 5imbi12d 345 . . 3 (𝑦 = 𝑧 → ((𝑦𝑅𝑥𝑦𝑅𝑥) ↔ (𝑧𝑅𝑥𝑧𝑅𝑥)))
7 breq2 5114 . . . 4 (𝑥 = 𝑧 → (𝑦𝑅𝑥𝑦𝑅𝑧))
8 breq2 5114 . . . 4 (𝑥 = 𝑧 → (𝑦𝑅𝑥𝑦𝑅𝑧))
97, 8imbi12d 345 . . 3 (𝑥 = 𝑧 → ((𝑦𝑅𝑥𝑦𝑅𝑥) ↔ (𝑦𝑅𝑧𝑦𝑅𝑧)))
106, 9alcomw 2048 . 2 (∀𝑦𝑥(𝑦𝑅𝑥𝑦𝑅𝑥) ↔ ∀𝑥𝑦(𝑦𝑅𝑥𝑦𝑅𝑥))
11 vex 3452 . . . . 5 𝑦 ∈ V
12 vex 3452 . . . . 5 𝑥 ∈ V
1311, 12brcnv 5843 . . . 4 (𝑦𝑅𝑥𝑥𝑅𝑦)
1413imbi1i 350 . . 3 ((𝑦𝑅𝑥𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦𝑦𝑅𝑥))
15142albii 1823 . 2 (∀𝑥𝑦(𝑦𝑅𝑥𝑦𝑅𝑥) ↔ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥))
163, 10, 153bitri 297 1 (𝑅𝑅 ↔ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540  wss 3915   class class class wbr 5110  ccnv 5637  Rel wrel 5643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-rel 5645  df-cnv 5646
This theorem is referenced by:  dfer2  8656  relcnveq3  36811  relcnveq  36812  relcnveq2  36813  cnvcosseq  36928  symrelcoss2  36957  elrelscnveq3  36982  elrelscnveq  36983  elrelscnveq2  36984  dfsymrels3  37037  dfsymrel3  37041  symrefref3  37055  refsymrels3  37057  elrefsymrels3  37061  dfeqvrels3  37080
  Copyright terms: Public domain W3C validator