MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ereq2 Structured version   Visualization version   GIF version

Theorem ereq2 8286
Description: Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.)
Assertion
Ref Expression
ereq2 (𝐴 = 𝐵 → (𝑅 Er 𝐴𝑅 Er 𝐵))

Proof of Theorem ereq2
StepHypRef Expression
1 eqeq2 2830 . . 3 (𝐴 = 𝐵 → (dom 𝑅 = 𝐴 ↔ dom 𝑅 = 𝐵))
213anbi2d 1432 . 2 (𝐴 = 𝐵 → ((Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅) ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐵 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)))
3 df-er 8278 . 2 (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
4 df-er 8278 . 2 (𝑅 Er 𝐵 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐵 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
52, 3, 43bitr4g 315 1 (𝐴 = 𝐵 → (𝑅 Er 𝐴𝑅 Er 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  w3a 1079   = wceq 1528  cun 3931  wss 3933  ccnv 5547  dom cdm 5548  ccom 5552  Rel wrel 5553   Er wer 8275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1081  df-ex 1772  df-cleq 2811  df-er 8278
This theorem is referenced by:  iserd  8304  efgval  18772  frgp0  18815  frgpmhm  18820
  Copyright terms: Public domain W3C validator