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 6081

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 2163. (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 6073	. . 3 ⊢ Rel ^◡𝑅
2		ssrel3 5745	. . 3 ⊢ (Rel ^◡𝑅 → (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥)))
3	1, 2	ax-mp 5	. 2 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥))
4		breq1 5103	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑦^◡𝑅𝑥 ↔ 𝑧^◡𝑅𝑥))
5		breq1 5103	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑧𝑅𝑥))
6	4, 5	imbi12d 344	. . 3 ⊢ (𝑦 = 𝑧 → ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑧^◡𝑅𝑥 → 𝑧𝑅𝑥)))
7		breq2 5104	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑦^◡𝑅𝑥 ↔ 𝑦^◡𝑅𝑧))
8		breq2 5104	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧))
9	7, 8	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑧 → ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑦^◡𝑅𝑧 → 𝑦𝑅𝑧)))
10	6, 9	alcomw 2047	. 2 ⊢ (∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥))
11		vex 3446	. . . . 5 ⊢ 𝑦 ∈ V
12		vex 3446	. . . . 5 ⊢ 𝑥 ∈ V
13	11, 12	brcnv 5841	. . . 4 ⊢ (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
14	13	imbi1i 349	. . 3 ⊢ ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦 → 𝑦𝑅𝑥))
15	14	2albii 1822	. 2 ⊢ (∀𝑥∀𝑦(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))
16	3, 10, 15	3bitri 297	1 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∀wal 1540 ⊆ wss 3903 class class class wbr 5100 ^◡ccnv 5633 Rel wrel 5639

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-sep 5245 ax-pr 5381

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-rab 3402 df-v 3444 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-sn 4583 df-pr 4585 df-op 4589 df-br 5101 df-opab 5163 df-xp 5640 df-rel 5641 df-cnv 5642

This theorem is referenced by: dfer2 8648 relcnveq3 38607 relcnveq 38608 relcnveq2 38609 cnvcosseq 38807 symrelcoss2 38836 dfsymrels3 38906 elrelscnveq3 38907 elrelscnveq 38908 elrelscnveq2 38909 dfsymrel3 38914 symrefref3 38928 refsymrels3 38930 elrefsymrels3 38934 dfeqvrels3 38953

W3C validator