Theorem eqrdv 2351

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

Syntax hints:   → wi 4   ↔ wb 176  ∀wal 1540   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-cleq 2346

This theorem is referenced by:  eqrdav  2352  csbcomg  3159  csbabg  3197  uneq1  3411  ineq1  3450  unineq  3505  difin2  3516  difsn  3845  intmin4  3955  iunconst  3977  iinconst  3978  dfiun2g  3999  iindif2  4035  iinin2  4036  iinxprg  4043  iunxsng  4044  xpkeq1  4198  xpkeq2  4199  eqpw1uni  4330  iotaeq  4347  nnsucelrlem2  4425  dfco2a  5081  imadif  5171  fun11iun  5305  unpreima  5408  inpreima  5409  respreima  5410  fconstfv  5456  funiunfv  5467  erdmrn  5965  enprmaplem5  6080  ncdisjun  6136  nmembers1lem3  6270