Theorem eqrdv 2020

Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)

Hypothesis

Ref	Expression
eqrdv.1	⊢ (φ → (x ∈ A ↔ x ∈ B))

Assertion

Ref	Expression
eqrdv	⊢ (φ → A = B)

Distinct variable groups:   x,A   x,B   φ,x

Proof of Theorem eqrdv

Step	Hyp	Ref	Expression
1		eqrdv.1	. . 3 ⊢ (φ → (x ∈ A ↔ x ∈ B))
2	1	alrimiv 1736	. 2 ⊢ (φ → ∀x(x ∈ A ↔ x ∈ B))
3		dfcleq 2016	. 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
4	2, 3	sylibr 137	1 ⊢ (φ → A = B)

Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1226   = wceq 1228   ∈ wcel 1374

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-17 1400  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-cleq 2015

This theorem is referenced by:  eqrdav  2021  csbcomg  2848  csbabg  2882  uneq1  3065  ineq1  3106  difin2  3174  difsn  3473  intmin4  3615  iunconstm  3637  iinconstm  3638  dfiun2g  3661  iindif2m  3696  iinin2m  3697  iunxsng  3704  iunpw  4159  opthprc  4316  inimasn  4666  dmsnopg  4717  dfco2a  4746  iotaeq  4800  fun11iun  5070  ssimaex  5157  unpreima  5215  respreima  5218  fconstfvm  5302  reldm  5733  rntpos  5792  frecsuclem3  5904  iserd  6041  erth  6059  ecidg  6079  genpassl  6377  genpassu  6378  1idprl  6427  1idpru  6428