Theorem eqrd 3944

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   = wceq 1541  Ⅎwnf 1789   ∈ wcel 2109  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-nf 1790  df-cleq 2731  df-clel 2817  df-nfc 2890

This theorem is referenced by:  eqri  3945  sniota  6421  dissnlocfin  22661  imasnopn  22822  imasncld  22823  imasncls  22824  blval2  23699  eqrrabd  30828  fimarab  30959  ofpreima  30981  zarcls  31803  ordtconnlem1  31853  qqhval2  31911  reprdifc  32586  topdifinfindis  35496  icorempo  35501  isbasisrelowllem1  35505  isbasisrelowllem2  35506  sticksstones11  40092  areaquad  41027  rfcnpre1  42515  rfcnpre2  42527  preimagelt  44190  preimalegt  44191