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

Theorem eqrd 3999
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 2202 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
4 eqrd.1 . . 3 𝑥𝐴
5 eqrd.2 . . 3 𝑥𝐵
64, 5cleqf 2924 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
73, 6sylibr 233 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1532   = wceq 1534  wnf 1778  wcel 2099  wnfc 2876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-11 2147  ax-12 2167  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-nf 1779  df-cleq 2718  df-clel 2803  df-nfc 2878
This theorem is referenced by:  eqri  4000  sniota  6545  dissnlocfin  23524  imasnopn  23685  imasncld  23686  imasncls  23687  blval2  24562  eqrrabd  32429  fimarab  32560  ofpreima  32582  algextdeglem6  33589  zarcls  33689  ordtconnlem1  33739  qqhval2  33797  reprdifc  34473  topdifinfindis  37053  icorempo  37058  isbasisrelowllem1  37062  isbasisrelowllem2  37063  sticksstones11  41854  areaquad  42881  rfcnpre1  44618  rfcnpre2  44630  preimagelt  46320  preimalegt  46321
  Copyright terms: Public domain W3C validator