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

Theorem dfeqvrel2 34962
Description: Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.)
Assertion
Ref Expression
dfeqvrel2 ( EqvRel 𝑅 ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅 ∧ (𝑅𝑅) ⊆ 𝑅) ∧ Rel 𝑅))

Proof of Theorem dfeqvrel2
StepHypRef Expression
1 df-eqvrel 34958 . 2 ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅))
2 refsymrel2 34941 . . . 4 (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅) ∧ Rel 𝑅))
3 dftrrel2 34951 . . . 4 ( TrRel 𝑅 ↔ ((𝑅𝑅) ⊆ 𝑅 ∧ Rel 𝑅))
42, 3anbi12i 620 . . 3 ((( RefRel 𝑅 ∧ SymRel 𝑅) ∧ TrRel 𝑅) ↔ (((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅) ∧ Rel 𝑅) ∧ ((𝑅𝑅) ⊆ 𝑅 ∧ Rel 𝑅)))
5 df-3an 1073 . . 3 (( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅) ↔ (( RefRel 𝑅 ∧ SymRel 𝑅) ∧ TrRel 𝑅))
6 df-3an 1073 . . . . 5 ((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅 ∧ (𝑅𝑅) ⊆ 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅) ∧ (𝑅𝑅) ⊆ 𝑅))
76anbi1i 617 . . . 4 (((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅 ∧ (𝑅𝑅) ⊆ 𝑅) ∧ Rel 𝑅) ↔ (((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅) ∧ (𝑅𝑅) ⊆ 𝑅) ∧ Rel 𝑅))
8 3anan32 1081 . . . 4 (((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅) ∧ Rel 𝑅 ∧ (𝑅𝑅) ⊆ 𝑅) ↔ (((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅) ∧ (𝑅𝑅) ⊆ 𝑅) ∧ Rel 𝑅))
9 anandi3r 1091 . . . 4 (((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅) ∧ Rel 𝑅 ∧ (𝑅𝑅) ⊆ 𝑅) ↔ (((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅) ∧ Rel 𝑅) ∧ ((𝑅𝑅) ⊆ 𝑅 ∧ Rel 𝑅)))
107, 8, 93bitr2i 291 . . 3 (((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅 ∧ (𝑅𝑅) ⊆ 𝑅) ∧ Rel 𝑅) ↔ (((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅) ∧ Rel 𝑅) ∧ ((𝑅𝑅) ⊆ 𝑅 ∧ Rel 𝑅)))
114, 5, 103bitr4i 295 . 2 (( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅 ∧ (𝑅𝑅) ⊆ 𝑅) ∧ Rel 𝑅))
121, 11bitri 267 1 ( EqvRel 𝑅 ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅𝑅𝑅 ∧ (𝑅𝑅) ⊆ 𝑅) ∧ Rel 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386  w3a 1071  wss 3792   I cid 5260  ccnv 5354  dom cdm 5355  cres 5357  ccom 5359  Rel wrel 5360   RefRel wrefrel 34612   SymRel wsymrel 34618   TrRel wtrrel 34621   EqvRel weqvrel 34623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-refrel 34890  df-symrel 34918  df-trrel 34948  df-eqvrel 34958
This theorem is referenced by:  eleqvrelsrel  34966  eqvrelrel  34967  eqvreltr  34977
  Copyright terms: Public domain W3C validator