Theorem eqrdv 2351

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

Hypothesis

Ref	Expression
eqrdv.1	|- (ph -> (x e. A <-> x e. B))

Assertion

Ref	Expression
eqrdv	|- (ph -> A = B)

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

Proof of Theorem eqrdv

Step	Hyp	Ref	Expression
1		eqrdv.1	. . 3 |- (ph -> (x e. A <-> x e. B))
2	1	alrimiv 1631	. 2 |- (ph -> A.x(x e. A <-> x e. B))
3		dfcleq 2347	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
4	2, 3	sylibr 203	1 |- (ph -> A = B)

Syntax hints:   -> wi 4   <-> wb 176  A.wal 1540   = wceq 1642   e. 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  3160  csbabg  3198  uneq1  3412  ineq1  3451  unineq  3506  difin2  3517  difsn  3846  intmin4  3956  iunconst  3978  iinconst  3979  dfiun2g  4000  iindif2  4036  iinin2  4037  iinxprg  4044  iunxsng  4045  xpkeq1  4199  xpkeq2  4200  eqpw1uni  4331  iotaeq  4348  nnsucelrlem2  4426  dfco2a  5082  imadif  5172  fun11iun  5306  unpreima  5409  inpreima  5410  respreima  5411  fconstfv  5457  funiunfv  5468  erdmrn  5966  enprmaplem5  6081  ncdisjun  6137  nmembers1lem3  6271