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

Theorem eqrelrdv 5139
Description: Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.)
Hypotheses
Ref Expression
eqrelrdv.1 Rel 𝐴
eqrelrdv.2 Rel 𝐵
eqrelrdv.3 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
Assertion
Ref Expression
eqrelrdv (𝜑𝐴 = 𝐵)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜑,𝑥,𝑦

Proof of Theorem eqrelrdv
StepHypRef Expression
1 eqrelrdv.3 . . 3 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
21alrimivv 1843 . 2 (𝜑 → ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3 eqrelrdv.1 . . 3 Rel 𝐴
4 eqrelrdv.2 . . 3 Rel 𝐵
5 eqrel 5132 . . 3 ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
63, 4, 5mp2an 704 . 2 (𝐴 = 𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
72, 6sylibr 223 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wal 1473   = wceq 1475  wcel 1977  cop 4131  Rel wrel 5043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-opab 4644  df-xp 5044  df-rel 5045
This theorem is referenced by:  eqbrrdiv  5141  fcnvres  5995  fmptco  6303  fpwwe2lem8  9338  fpwwe2lem12  9342  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  gsumcom2  18197  lgsquadlem1  24905  lgsquadlem2  24906  fmptcof2  28839  dfcnv2  28859  dih1dimatlem  35636
  Copyright terms: Public domain W3C validator