Theorem refrelsredund2 38631

Description: The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 38511) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.)

Assertion

Ref	Expression
refrelsredund2	⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , EqvRels ⟩

Proof of Theorem refrelsredund2

Step	Hyp	Ref	Expression
1		refrelsredund4 38630	. 2 ⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , ( RefRels ∩ SymRels )⟩
2		df-eqvrels 38582	. . . 4 ⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )
3		inss1 4203	. . . 4 ⊢ (( RefRels ∩ SymRels ) ∩ TrRels ) ⊆ ( RefRels ∩ SymRels )
4	2, 3	eqsstri 3996	. . 3 ⊢ EqvRels ⊆ ( RefRels ∩ SymRels )
5	4	redundss3 38626	. 2 ⊢ ({𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , ( RefRels ∩ SymRels )⟩ → {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , EqvRels ⟩)
6	1, 5	ax-mp 5	1 ⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , EqvRels ⟩

Syntax hints:  {crab 3408   ∩ cin 3916   ⊆ wss 3917   I cid 5535  dom cdm 5641   ↾ cres 5643   Rels crels 38178   RefRels crefrels 38181   SymRels csymrels 38187   TrRels ctrrels 38190   EqvRels ceqvrels 38192   Redund wredund 38197

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-10 2142  ax-11 2158  ax-12 2178  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-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-rels 38483  df-ssr 38496  df-refs 38508  df-refrels 38509  df-syms 38540  df-symrels 38541  df-eqvrels 38582  df-redund 38622

This theorem is referenced by:  refrelsredund3  38632