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 6088

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 6078	. . 3 ⊢ Rel ^◡𝑅
2		ssrel3 5752	. . 3 ⊢ (Rel ^◡𝑅 → (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥)))
3	1, 2	ax-mp 5	. 2 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥))
4		breq1 5113	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑦^◡𝑅𝑥 ↔ 𝑧^◡𝑅𝑥))
5		breq1 5113	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑧𝑅𝑥))
6	4, 5	imbi12d 344	. . 3 ⊢ (𝑦 = 𝑧 → ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑧^◡𝑅𝑥 → 𝑧𝑅𝑥)))
7		breq2 5114	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑦^◡𝑅𝑥 ↔ 𝑦^◡𝑅𝑧))
8		breq2 5114	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧))
9	7, 8	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑧 → ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑦^◡𝑅𝑧 → 𝑦𝑅𝑧)))
10	6, 9	alcomw 2045	. 2 ⊢ (∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥))
11		vex 3454	. . . . 5 ⊢ 𝑦 ∈ V
12		vex 3454	. . . . 5 ⊢ 𝑥 ∈ V
13	11, 12	brcnv 5849	. . . 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 3917 class class class wbr 5110 ^◡ccnv 5640 Rel wrel 5646

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 2702 ax-sep 5254 ax-nul 5264 ax-pr 5390

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 2709 df-cleq 2722 df-clel 2804 df-rab 3409 df-v 3452 df-dif 3920 df-un 3922 df-ss 3934 df-nul 4300 df-if 4492 df-sn 4593 df-pr 4595 df-op 4599 df-br 5111 df-opab 5173 df-xp 5647 df-rel 5648 df-cnv 5649

This theorem is referenced by: dfer2 8675 relcnveq3 38316 relcnveq 38317 relcnveq2 38318 cnvcosseq 38435 symrelcoss2 38464 elrelscnveq3 38489 elrelscnveq 38490 elrelscnveq2 38491 dfsymrels3 38544 dfsymrel3 38548 symrefref3 38562 refsymrels3 38564 elrefsymrels3 38568 dfeqvrels3 38587

W3C validator