Theorem eqrdv 2021

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 1737	. 2 ⊢ (φ → ∀x(x ∈ A ↔ x ∈ B))
3		dfcleq 2017	. 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 1375

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 1401  ax-ext 2005

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

This theorem is referenced by:  eqrdav  2022  csbcomg  2849  csbabg  2883  uneq1  3066  ineq1  3107  difin2  3175  difsn  3474  intmin4  3616  iunconstm  3638  iinconstm  3639  dfiun2g  3662  iindif2m  3697  iinin2m  3698  iunxsng  3705  iunpw  4159  opthprc  4316  inimasn  4666  dmsnopg  4717  dfco2a  4746  iotaeq  4800  fun11iun  5070  ssimaex  5157  unpreima  5215  respreima  5218  fconstfvm  5302  reldm  5732  rntpos  5791  frecsuclem3  5901  iserd  6038  erth  6055