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 6063

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 2158. (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 6055	. . 3 ⊢ Rel ^◡𝑅
2		ssrel3 5729	. . 3 ⊢ (Rel ^◡𝑅 → (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥)))
3	1, 2	ax-mp 5	. 2 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥))
4		breq1 5095	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑦^◡𝑅𝑥 ↔ 𝑧^◡𝑅𝑥))
5		breq1 5095	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑧𝑅𝑥))
6	4, 5	imbi12d 344	. . 3 ⊢ (𝑦 = 𝑧 → ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑧^◡𝑅𝑥 → 𝑧𝑅𝑥)))
7		breq2 5096	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑦^◡𝑅𝑥 ↔ 𝑦^◡𝑅𝑧))
8		breq2 5096	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧))
9	7, 8	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑧 → ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑦^◡𝑅𝑧 → 𝑦𝑅𝑧)))
10	6, 9	alcomw 2045	. 2 ⊢ (∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥))
11		vex 3440	. . . . 5 ⊢ 𝑦 ∈ V
12		vex 3440	. . . . 5 ⊢ 𝑥 ∈ V
13	11, 12	brcnv 5825	. . . 4 ⊢ (𝑦^◡𝑅𝑥 ↔ 𝑥𝑅𝑦)
14	13	imbi1i 349	. . 3 ⊢ ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑦 → 𝑦𝑅𝑥))
15	14	2albii 1820	. 2 ⊢ (∀𝑥∀𝑦(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))
16	3, 10, 15	3bitri 297	1 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 ⊆ wss 3903 class class class wbr 5092 ^◡ccnv 5618 Rel wrel 5624

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2701 ax-sep 5235 ax-nul 5245 ax-pr 5371

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-rab 3395 df-v 3438 df-dif 3906 df-un 3908 df-ss 3920 df-nul 4285 df-if 4477 df-sn 4578 df-pr 4580 df-op 4584 df-br 5093 df-opab 5155 df-xp 5625 df-rel 5626 df-cnv 5627

This theorem is referenced by: dfer2 8626 relcnveq3 38315 relcnveq 38316 relcnveq2 38317 cnvcosseq 38434 symrelcoss2 38463 elrelscnveq3 38488 elrelscnveq 38489 elrelscnveq2 38490 dfsymrels3 38543 dfsymrel3 38547 symrefref3 38561 refsymrels3 38563 elrefsymrels3 38567 dfeqvrels3 38586

W3C validator