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

Theorem eqrd 3914
Description: Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.) (Proof shortened by BJ, 1-Dec-2021.)
Hypotheses
Ref Expression
eqrd.0 𝑥𝜑
eqrd.1 𝑥𝐴
eqrd.2 𝑥𝐵
eqrd.3 (𝜑 → (𝑥𝐴𝑥𝐵))
Assertion
Ref Expression
eqrd (𝜑𝐴 = 𝐵)

Proof of Theorem eqrd
StepHypRef Expression
1 eqrd.0 . . 3 𝑥𝜑
2 eqrd.3 . . 3 (𝜑 → (𝑥𝐴𝑥𝐵))
31, 2alrimi 2180 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
4 eqrd.1 . . 3 𝑥𝐴
5 eqrd.2 . . 3 𝑥𝐵
64, 5cleqf 2980 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
73, 6sylibr 235 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1523   = wceq 1525  wnf 1769  wcel 2083  wnfc 2935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-11 2128  ax-12 2143  ax-ext 2771
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-cleq 2790  df-clel 2865  df-nfc 2937
This theorem is referenced by:  sniota  6223  dissnlocfin  21825  imasnopn  21986  imasncld  21987  imasncls  21988  blval2  22859  eqri  29919  fimarab  30076  ofpreima  30096  ordtconnlem1  30780  qqhval2  30836  reprdifc  31511  topdifinfindis  34179  icorempo  34184  isbasisrelowllem1  34188  isbasisrelowllem2  34189  areaquad  39329  rfcnpre1  40836  rfcnpre2  40848  preimagelt  42544  preimalegt  42545
  Copyright terms: Public domain W3C validator