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  6564  1idpru  6565  eqreznegel  8285  iccid  8524  fzsplit2  8644  fzsn  8659  fzpr  8669  uzsplit  8684  fzoval  8735  frec2uzrand  8832