Theorem eqrdv 2020

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 1736	. 2 |- (ph -> A.x(x e. A <-> x e. B))
3		dfcleq 2016	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
4	2, 3	sylibr 137	1 |- (ph -> A = B)

Syntax hints:   -> wi 4   <-> wb 98  A.wal 1226   = wceq 1228   e. wcel 1374

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 1400  ax-ext 2004

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

This theorem is referenced by:  eqrdav  2021  csbcomg  2850  csbabg  2884  uneq1  3067  ineq1  3108  difin2  3176  difsn  3475  intmin4  3617  iunconstm  3639  iinconstm  3640  dfiun2g  3663  iindif2m  3698  iinin2m  3699  iunxsng  3706  iunpw  4161  opthprc  4318  inimasn  4668  dmsnopg  4719  dfco2a  4748  iotaeq  4802  fun11iun  5072  ssimaex  5159  unpreima  5217  respreima  5220  fconstfvm  5304  reldm  5735  rntpos  5794  frecsuclem3  5906  iserd  6043  erth  6061  ecidg  6081  genpassl  6379  genpassu  6380  1idprl  6429  1idpru  6430