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 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 2170. (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.

Step	Hyp	Ref	Expression
1		relcnv 6063	. . 3 ⊢ Rel ^◡𝑅
2		ssrel3 5732	. . 3 ⊢ (Rel ^◡𝑅 → (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥)))
3	1, 2	ax-mp 5	. 2 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥))
4		breq1 5078	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑦^◡𝑅𝑥 ↔ 𝑧^◡𝑅𝑥))
5		breq1 5078	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑧𝑅𝑥))
6	4, 5	imbi12d 346	. . 3 ⊢ (𝑦 = 𝑧 → ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑧^◡𝑅𝑥 → 𝑧𝑅𝑥)))
7		breq2 5079	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑦^◡𝑅𝑥 ↔ 𝑦^◡𝑅𝑧))
8		breq2 5079	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧))
9	7, 8	imbi12d 346	. . 3 ⊢ (𝑥 = 𝑧 → ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑦^◡𝑅𝑧 → 𝑦𝑅𝑧)))
10	6, 9	alcomw 2053	. 2 ⊢ (∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥))
11		vex 3437	. . . . 5 ⊢ 𝑦 ∈ V
12		vex 3437	. . . . 5 ⊢ 𝑥 ∈ V
13	11, 12	brcnv 5827	. . . 4 ⊢ (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
14	13	imbi1i 351	. . 3 ⊢ ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦 → 𝑦𝑅𝑥))
15	14	2albii 1828	. 2 ⊢ (∀𝑥∀𝑦(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))
16	3, 10, 15	3bitri 299	1 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∀wal 1546 ⊆ wss 3885 class class class wbr 5075 ^◡ccnv 5620 Rel wrel 5626

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-ext 2713 ax-sep 5221 ax-pr 5365

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-sb 2075 df-clab 2720 df-cleq 2733 df-clel 2816 df-rab 3394 df-v 3435 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-nul 4265 df-if 4458 df-sn 4559 df-pr 4561 df-op 4565 df-br 5076 df-opab 5138 df-xp 5627 df-rel 5628 df-cnv 5629

This theorem is referenced by: dfer2 8638 relcnveq3 38709 relcnveq 38710 relcnveq2 38711 cnvcosseq 38909 symrelcoss2 38938 dfsymrels3 39008 elrelscnveq3 39009 elrelscnveq 39010 elrelscnveq2 39011 dfsymrel3 39016 symrefref3 39030 refsymrels3 39032 elrefsymrels3 39036 dfeqvrels3 39055

W3C validator