Theorem eqrd 3955

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1558   = wceq 1560  Ⅎwnf 1803   ∈ wcel 2142  Ⅎwnfc 2909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-cleq 2754  df-clel 2837  df-nfc 2911

This theorem is referenced by:  eqri  3956  eqrrabd  4039  sniota  6512  fimarab  6941  dissnlocfin  23589  imasnopn  23750  imasncld  23751  imasncls  23752  blval2  24622  ofpreima  32867  algextdeglem6  34019  constrfin  34043  zarcls  34171  ordtconnlem1  34221  qqhval2  34279  reprdifc  34921  topdifinfindis  37840  icorempo  37845  isbasisrelowllem1  37849  isbasisrelowllem2  37850  sticksstones11  42773  areaquad  43793  rfcnpre1  45599  rfcnpre2  45611  preimagelt  47273  preimalegt  47274