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

Theorem eqrd 4003
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 2213 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
4 eqrd.1 . . 3 𝑥𝐴
5 eqrd.2 . . 3 𝑥𝐵
64, 5cleqf 2934 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
73, 6sylibr 234 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538   = wceq 1540  wnf 1783  wcel 2108  wnfc 2890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2729  df-clel 2816  df-nfc 2892
This theorem is referenced by:  eqri  4004  eqrrabd  4086  sniota  6552  fimarab  6983  dissnlocfin  23537  imasnopn  23698  imasncld  23699  imasncls  23700  blval2  24575  ofpreima  32675  algextdeglem6  33763  constrfin  33787  zarcls  33873  ordtconnlem1  33923  qqhval2  33983  reprdifc  34642  topdifinfindis  37347  icorempo  37352  isbasisrelowllem1  37356  isbasisrelowllem2  37357  sticksstones11  42157  areaquad  43228  rfcnpre1  45024  rfcnpre2  45036  preimagelt  46714  preimalegt  46715
  Copyright terms: Public domain W3C validator