Theorem eqrd 3914

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 2180	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		eqrd.1	. . 3 ⊢ Ⅎ𝑥𝐴
5		eqrd.2	. . 3 ⊢ Ⅎ𝑥𝐵
6	4, 5	cleqf 2980	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
7	3, 6	sylibr 235	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1523   = wceq 1525  Ⅎwnf 1769   ∈ wcel 2083  Ⅎwnfc 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-cleq 2790  df-clel 2865  df-nfc 2937

This theorem is referenced by:  sniota  6223  dissnlocfin  21825  imasnopn  21986  imasncld  21987  imasncls  21988  blval2  22859  eqri  29919  fimarab  30076  ofpreima  30096  ordtconnlem1  30780  qqhval2  30836  reprdifc  31511  topdifinfindis  34179  icorempo  34184  isbasisrelowllem1  34188  isbasisrelowllem2  34189  areaquad  39329  rfcnpre1  40836  rfcnpre2  40848  preimagelt  42544  preimalegt  42545