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

Theorem eqrd 4015
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 2211 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
4 eqrd.1 . . 3 𝑥𝐴
5 eqrd.2 . . 3 𝑥𝐵
64, 5cleqf 2932 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
73, 6sylibr 234 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535   = wceq 1537  wnf 1780  wcel 2106  wnfc 2888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-cleq 2727  df-clel 2814  df-nfc 2890
This theorem is referenced by:  eqri  4016  eqrrabd  4096  sniota  6554  fimarab  6983  dissnlocfin  23553  imasnopn  23714  imasncld  23715  imasncls  23716  blval2  24591  ofpreima  32682  algextdeglem6  33728  constrfin  33751  zarcls  33835  ordtconnlem1  33885  qqhval2  33945  reprdifc  34621  topdifinfindis  37329  icorempo  37334  isbasisrelowllem1  37338  isbasisrelowllem2  37339  sticksstones11  42138  areaquad  43205  rfcnpre1  44957  rfcnpre2  44969  preimagelt  46655  preimalegt  46656
  Copyright terms: Public domain W3C validator