Theorem eqrdv 2035

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 1751	. 2 ⊢ (φ → ∀x(x ∈ A ↔ x ∈ B))
3		dfcleq 2031	. 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
4	2, 3	sylibr 137	1 ⊢ (φ → A = B)

Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1240   = wceq 1242   ∈ wcel 1390

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 1333  ax-gen 1335  ax-17 1416  ax-ext 2019

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

This theorem is referenced by:  eqrdav  2036  csbcomg  2867  csbabg  2901  uneq1  3084  ineq1  3125  difin2  3193  difsn  3492  intmin4  3634  iunconstm  3656  iinconstm  3657  dfiun2g  3680  iindif2m  3715  iinin2m  3716  iunxsng  3723  iunpw  4177  opthprc  4334  inimasn  4684  dmsnopg  4735  dfco2a  4764  iotaeq  4818  fun11iun  5090  ssimaex  5177  unpreima  5235  respreima  5238  fconstfvm  5322  reldm  5754  rntpos  5813  frecsuclem3  5929  iserd  6068  erth  6086  ecidg  6106  genpassl  6507  genpassu  6508  1idprl  6566  1idpru  6567  eqreznegel  8325  iccid  8564  fzsplit2  8684  fzsn  8699  fzpr  8709  uzsplit  8724  fzoval  8775  frec2uzrand  8872