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

Theorem cnvsym 6119
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 2146. (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 6109 . . 3 Rel 𝑅
2 ssrel3 5788 . . 3 (Rel 𝑅 → (𝑅𝑅 ↔ ∀𝑦𝑥(𝑦𝑅𝑥𝑦𝑅𝑥)))
31, 2ax-mp 5 . 2 (𝑅𝑅 ↔ ∀𝑦𝑥(𝑦𝑅𝑥𝑦𝑅𝑥))
4 breq1 5152 . . . 4 (𝑦 = 𝑧 → (𝑦𝑅𝑥𝑧𝑅𝑥))
5 breq1 5152 . . . 4 (𝑦 = 𝑧 → (𝑦𝑅𝑥𝑧𝑅𝑥))
64, 5imbi12d 343 . . 3 (𝑦 = 𝑧 → ((𝑦𝑅𝑥𝑦𝑅𝑥) ↔ (𝑧𝑅𝑥𝑧𝑅𝑥)))
7 breq2 5153 . . . 4 (𝑥 = 𝑧 → (𝑦𝑅𝑥𝑦𝑅𝑧))
8 breq2 5153 . . . 4 (𝑥 = 𝑧 → (𝑦𝑅𝑥𝑦𝑅𝑧))
97, 8imbi12d 343 . . 3 (𝑥 = 𝑧 → ((𝑦𝑅𝑥𝑦𝑅𝑥) ↔ (𝑦𝑅𝑧𝑦𝑅𝑧)))
106, 9alcomw 2039 . 2 (∀𝑦𝑥(𝑦𝑅𝑥𝑦𝑅𝑥) ↔ ∀𝑥𝑦(𝑦𝑅𝑥𝑦𝑅𝑥))
11 vex 3465 . . . . 5 𝑦 ∈ V
12 vex 3465 . . . . 5 𝑥 ∈ V
1311, 12brcnv 5885 . . . 4 (𝑦𝑅𝑥𝑥𝑅𝑦)
1413imbi1i 348 . . 3 ((𝑦𝑅𝑥𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦𝑦𝑅𝑥))
15142albii 1814 . 2 (∀𝑥𝑦(𝑦𝑅𝑥𝑦𝑅𝑥) ↔ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥))
163, 10, 153bitri 296 1 (𝑅𝑅 ↔ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1531  wss 3944   class class class wbr 5149  ccnv 5677  Rel wrel 5683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-xp 5684  df-rel 5685  df-cnv 5686
This theorem is referenced by:  dfer2  8726  relcnveq3  37923  relcnveq  37924  relcnveq2  37925  cnvcosseq  38039  symrelcoss2  38068  elrelscnveq3  38093  elrelscnveq  38094  elrelscnveq2  38095  dfsymrels3  38148  dfsymrel3  38152  symrefref3  38166  refsymrels3  38168  elrefsymrels3  38172  dfeqvrels3  38191
  Copyright terms: Public domain W3C validator