Theorem eqrd 3969

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

Step	Hyp	Ref	Expression
1		eqrd.0	. . 3 ⊢ Ⅎ𝑥𝜑
2		eqrd.3	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	alrimi 2214	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		eqrd.1	. . 3 ⊢ Ⅎ𝑥𝐴
5		eqrd.2	. . 3 ⊢ Ⅎ𝑥𝐵
6	4, 5	cleqf 2921	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
7	3, 6	sylibr 234	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2877

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 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2722  df-clel 2804  df-nfc 2879

This theorem is referenced by:  eqri  3970  eqrrabd  4052  sniota  6505  fimarab  6938  dissnlocfin  23423  imasnopn  23584  imasncld  23585  imasncls  23586  blval2  24457  ofpreima  32596  algextdeglem6  33719  constrfin  33743  zarcls  33871  ordtconnlem1  33921  qqhval2  33979  reprdifc  34625  topdifinfindis  37341  icorempo  37346  isbasisrelowllem1  37350  isbasisrelowllem2  37351  sticksstones11  42151  areaquad  43212  rfcnpre1  45020  rfcnpre2  45032  preimagelt  46704  preimalegt  46705