Theorem elrefsymrels3 38566

Description: Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels3 38585) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrels3 38510, cf. the comment of dfrefrel3 38512. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
elrefsymrels3	⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels ))

Distinct variable group:   𝑥,𝑅,𝑦

Proof of Theorem elrefsymrels3

Step	Hyp	Ref	Expression
1		elrefsymrels2 38565	. 2 ⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels ))
2		idrefALT 6139	. . . 4 ⊢ (( I ↾ dom 𝑅) ⊆ 𝑅 ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥)
3		cnvsym 6140	. . . 4 ⊢ (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥))
4	2, 3	anbi12i 628	. . 3 ⊢ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ↔ (∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)))
5	4	anbi1i 624	. 2 ⊢ (((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels ))
6	1, 5	bitri 275	1 ⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels ))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1537   ∈ wcel 2108  ∀wral 3061   ∩ cin 3965   ⊆ wss 3966   class class class wbr 5151   I cid 5586  ^◡ccnv 5692  dom cdm 5693   ↾ cres 5695   Rels crels 38178   RefRels crefrels 38181   SymRels csymrels 38187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2157  ax-ext 2708  ax-sep 5305  ax-nul 5315  ax-pr 5441

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3483  df-dif 3969  df-un 3971  df-in 3973  df-ss 3983  df-nul 4343  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-br 5152  df-opab 5214  df-id 5587  df-xp 5699  df-rel 5700  df-cnv 5701  df-dm 5703  df-rn 5704  df-res 5705  df-rels 38481  df-ssr 38494  df-refs 38506  df-refrels 38507  df-syms 38538  df-symrels 38539

This theorem is referenced by: (None)