Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfeqvrels2 Structured version   Visualization version   GIF version

Theorem dfeqvrels2 34819
Description: Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.)
Assertion
Ref Expression
dfeqvrels2 EqvRels = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟𝑟𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}

Proof of Theorem dfeqvrels2
StepHypRef Expression
1 df-eqvrels 34816 . . 3 EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )
2 refsymrels2 34798 . . . 4 ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟𝑟𝑟)}
3 dftrrels2 34808 . . . 4 TrRels = {𝑟 ∈ Rels ∣ (𝑟𝑟) ⊆ 𝑟}
42, 3ineq12i 4009 . . 3 (( RefRels ∩ SymRels ) ∩ TrRels ) = ({𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟𝑟𝑟)} ∩ {𝑟 ∈ Rels ∣ (𝑟𝑟) ⊆ 𝑟})
5 inrab 4098 . . 3 ({𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟𝑟𝑟)} ∩ {𝑟 ∈ Rels ∣ (𝑟𝑟) ⊆ 𝑟}) = {𝑟 ∈ Rels ∣ ((( I ↾ dom 𝑟) ⊆ 𝑟𝑟𝑟) ∧ (𝑟𝑟) ⊆ 𝑟)}
61, 4, 53eqtri 2824 . 2 EqvRels = {𝑟 ∈ Rels ∣ ((( I ↾ dom 𝑟) ⊆ 𝑟𝑟𝑟) ∧ (𝑟𝑟) ⊆ 𝑟)}
7 df-3an 1110 . . 3 ((( I ↾ dom 𝑟) ⊆ 𝑟𝑟𝑟 ∧ (𝑟𝑟) ⊆ 𝑟) ↔ ((( I ↾ dom 𝑟) ⊆ 𝑟𝑟𝑟) ∧ (𝑟𝑟) ⊆ 𝑟))
87rabbii 3368 . 2 {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟𝑟𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)} = {𝑟 ∈ Rels ∣ ((( I ↾ dom 𝑟) ⊆ 𝑟𝑟𝑟) ∧ (𝑟𝑟) ⊆ 𝑟)}
96, 8eqtr4i 2823 1 EqvRels = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟𝑟𝑟 ∧ (𝑟𝑟) ⊆ 𝑟)}
Colors of variables: wff setvar class
Syntax hints:  wa 385  w3a 1108   = wceq 1653  {crab 3092  cin 3767  wss 3768   I cid 5218  ccnv 5310  dom cdm 5311  cres 5313  ccom 5315   Rels crels 34464   RefRels crefrels 34467   SymRels csymrels 34473   TrRels ctrrels 34476   EqvRels ceqvrels 34478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-sep 4974  ax-nul 4982  ax-pr 5096
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3386  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-op 4374  df-br 4843  df-opab 4905  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-rels 34722  df-ssr 34735  df-refs 34747  df-refrels 34748  df-syms 34775  df-symrels 34776  df-trs 34805  df-trrels 34806  df-eqvrels 34816
This theorem is referenced by:  dfeqvrels3  34820  eleqvrels2  34823
  Copyright terms: Public domain W3C validator