cnvsym - Metamath Proof Explorer

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

Theorem cnvsym 5960

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**
Step	Hyp	Ref	Expression
1		alcom 2163	. 2 ⊢ (∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅) ↔ ∀𝑥∀𝑦(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
2		relcnv 5953	. . 3 ⊢ Rel ^◡𝑅
3		ssrel 5643	. . 3 ⊢ (Rel ^◡𝑅 → (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅)))
4	2, 3	ax-mp 5	. 2 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
5		vex 3489	. . . . . 6 ⊢ 𝑦 ∈ V
6		vex 3489	. . . . . 6 ⊢ 𝑥 ∈ V
7	5, 6	brcnv 5739	. . . . 5 ⊢ (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
8		df-br 5053	. . . . 5 ⊢ (𝑦^◡𝑅𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ ^◡𝑅)
9	7, 8	bitr3i 279	. . . 4 ⊢ (𝑥𝑅𝑦 ↔ ⟨𝑦, 𝑥⟩ ∈ ^◡𝑅)
10		df-br 5053	. . . 4 ⊢ (𝑦𝑅𝑥 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅)
11	9, 10	imbi12i 353	. . 3 ⊢ ((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ↔ (⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
12	11	2albii 1821	. 2 ⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(⟨𝑦, 𝑥⟩ ∈ ^◡𝑅 → ⟨𝑦, 𝑥⟩ ∈ 𝑅))
13	1, 4, 12	3bitr4i 305	1 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∀wal 1535 ∈ wcel 2114 ⊆ wss 3924 ⟨cop 4559 class class class wbr 5052 ^◡ccnv 5540 Rel wrel 5546

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5189 ax-nul 5196 ax-pr 5316

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3488 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-nul 4280 df-if 4454 df-sn 4554 df-pr 4556 df-op 4560 df-br 5053 df-opab 5115 df-xp 5547 df-rel 5548 df-cnv 5549

This theorem is referenced by: dfer2 8276 relcnveq3 35610 relcnveq 35611 relcnveq2 35612 cnvcosseq 35714 symrelcoss2 35738 elrelscnveq3 35763 elrelscnveq 35764 elrelscnveq2 35765 dfsymrels3 35814 dfsymrel3 35818 symrefref3 35832 refsymrels3 35834 elrefsymrels3 35838 dfeqvrels3 35856

W3C validator