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 6072

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 6064	. . 3 ⊢ Rel ^◡𝑅
2		ssrel3 5736	. . 3 ⊢ (Rel ^◡𝑅 → (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥)))
3	1, 2	ax-mp 5	. 2 ⊢ (^◡𝑅 ⊆ 𝑅 ↔ ∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥))
4		breq1 5102	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑦^◡𝑅𝑥 ↔ 𝑧^◡𝑅𝑥))
5		breq1 5102	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑧𝑅𝑥))
6	4, 5	imbi12d 344	. . 3 ⊢ (𝑦 = 𝑧 → ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑧^◡𝑅𝑥 → 𝑧𝑅𝑥)))
7		breq2 5103	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑦^◡𝑅𝑥 ↔ 𝑦^◡𝑅𝑧))
8		breq2 5103	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧))
9	7, 8	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑧 → ((𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ (𝑦^◡𝑅𝑧 → 𝑦𝑅𝑧)))
10	6, 9	alcomw 2047	. 2 ⊢ (∀𝑦∀𝑥(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦(𝑦^◡𝑅𝑥 → 𝑦𝑅𝑥))
11		vex 3445	. . . . 5 ⊢ 𝑦 ∈ V
12		vex 3445	. . . . 5 ⊢ 𝑥 ∈ V
13	11, 12	brcnv 5832	. . . 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 3902 class class class wbr 5099 ^◡ccnv 5624 Rel wrel 5630

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 5242 ax-nul 5252 ax-pr 5378

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 3401 df-v 3443 df-dif 3905 df-un 3907 df-ss 3919 df-nul 4287 df-if 4481 df-sn 4582 df-pr 4584 df-op 4588 df-br 5100 df-opab 5162 df-xp 5631 df-rel 5632 df-cnv 5633

This theorem is referenced by: dfer2 8639 relcnveq3 38541 relcnveq 38542 relcnveq2 38543 cnvcosseq 38741 symrelcoss2 38770 dfsymrels3 38840 elrelscnveq3 38841 elrelscnveq 38842 elrelscnveq2 38843 dfsymrel3 38848 symrefref3 38862 refsymrels3 38864 elrefsymrels3 38868 dfeqvrels3 38887

W3C validator