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

Theorem cnvsym 5971
 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.)
Assertion
Ref Expression
cnvsym (𝑅𝑅 ↔ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥))
Distinct variable group:   𝑥,𝑦,𝑅

Proof of Theorem cnvsym
StepHypRef Expression
1 alcom 2155 . 2 (∀𝑦𝑥(⟨𝑦, 𝑥⟩ ∈ 𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅) ↔ ∀𝑥𝑦(⟨𝑦, 𝑥⟩ ∈ 𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
2 relcnv 5964 . . 3 Rel 𝑅
3 ssrel 5655 . . 3 (Rel 𝑅 → (𝑅𝑅 ↔ ∀𝑦𝑥(⟨𝑦, 𝑥⟩ ∈ 𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅)))
42, 3ax-mp 5 . 2 (𝑅𝑅 ↔ ∀𝑦𝑥(⟨𝑦, 𝑥⟩ ∈ 𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
5 vex 3502 . . . . . 6 𝑦 ∈ V
6 vex 3502 . . . . . 6 𝑥 ∈ V
75, 6brcnv 5751 . . . . 5 (𝑦𝑅𝑥𝑥𝑅𝑦)
8 df-br 5063 . . . . 5 (𝑦𝑅𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
97, 8bitr3i 278 . . . 4 (𝑥𝑅𝑦 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
10 df-br 5063 . . . 4 (𝑦𝑅𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
119, 10imbi12i 352 . . 3 ((𝑥𝑅𝑦𝑦𝑅𝑥) ↔ (⟨𝑦, 𝑥⟩ ∈ 𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
12112albii 1814 . 2 (∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥) ↔ ∀𝑥𝑦(⟨𝑦, 𝑥⟩ ∈ 𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
131, 4, 123bitr4i 304 1 (𝑅𝑅 ↔ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1528   ∈ wcel 2107   ⊆ wss 3939  ⟨cop 4569   class class class wbr 5062  ◡ccnv 5552  Rel wrel 5558 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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pr 5325 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063  df-opab 5125  df-xp 5559  df-rel 5560  df-cnv 5561 This theorem is referenced by:  dfer2  8283  relcnveq3  35448  relcnveq  35449  relcnveq2  35450  cnvcosseq  35551  symrelcoss2  35575  elrelscnveq3  35600  elrelscnveq  35601  elrelscnveq2  35602  dfsymrels3  35651  dfsymrel3  35655  symrefref3  35669  refsymrels3  35671  elrefsymrels3  35675  dfeqvrels3  35693
 Copyright terms: Public domain W3C validator