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

Theorem eqrd 3961
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 2206 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
4 eqrd.1 . . 3 𝑥𝐴
5 eqrd.2 . . 3 𝑥𝐵
64, 5cleqf 2936 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
73, 6sylibr 233 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1539   = wceq 1541  wnf 1785  wcel 2106  wnfc 2885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-12 2171  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-cleq 2729  df-clel 2815  df-nfc 2887
This theorem is referenced by:  eqri  3962  sniota  6484  dissnlocfin  22831  imasnopn  22992  imasncld  22993  imasncls  22994  blval2  23869  eqrrabd  31257  fimarab  31386  ofpreima  31408  zarcls  32258  ordtconnlem1  32308  qqhval2  32366  reprdifc  33043  topdifinfindis  35748  icorempo  35753  isbasisrelowllem1  35757  isbasisrelowllem2  35758  sticksstones11  40495  areaquad  41452  rfcnpre1  43128  rfcnpre2  43140  preimagelt  44834  preimalegt  44835
  Copyright terms: Public domain W3C validator