Theorem eqrdv 2186

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

Hypothesis

Ref	Expression
eqrdv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Assertion

Ref	Expression
eqrdv	⊢ (𝜑 → 𝐴 = 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Proof of Theorem eqrdv

Step	Hyp	Ref	Expression
1		eqrdv.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	alrimiv 1884	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfcleq 2182	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	2, 3	sylibr 134	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1361   = wceq 1363   ∈ wcel 2159

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-17 1536  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-cleq 2181

This theorem is referenced by:  eqrdav  2187  eqabdv  2317  csbcomg  3094  csbabg  3132  uneq1  3296  ineq1  3343  difin2  3411  difsn  3743  intmin4  3886  iunconstm  3908  iinconstm  3909  dfiun2g  3932  iindif2m  3968  iinin2m  3969  iunxsng  3976  iunxsngf  3978  iunpw  4494  opthprc  4691  inimasn  5060  dmsnopg  5114  dfco2a  5143  iotaeq  5200  fun11iun  5496  ssimaex  5592  unpreima  5656  respreima  5659  fconstfvm  5749  reldm  6204  rntpos  6275  frecsuclem  6424  iserd  6578  erth  6596  ecidg  6616  mapdm0  6680  map0e  6703  ixpiinm  6741  fifo  6996  ordiso2  7051  ctssdccl  7127  ctssdc  7129  exmidapne  7276  genpassl  7540  genpassu  7541  1idprl  7606  1idpru  7607  sup3exmid  8931  eqreznegel  9631  iccid  9942  fzsplit2  10067  fzsn  10083  fzpr  10094  uzsplit  10109  fzoval  10165  frec2uzrand  10422  infssuzex  11967  mhmpropd  12883  eqgid  13130  ghmmhmb  13153  ghmpropd  13182  ablnsg  13231  opprsubgg  13394  opprunitd  13420  unitpropdg  13458  opprsubrngg  13518  subsubrng2  13522  subrngpropd  13523  subsubrg2  13553  subrgpropd  13555  lssats2  13690  lsspropdg  13707  discld  14019  restsn  14063  restdis  14067  cndis  14124  cnpdis  14125  tx1cn  14152  tx2cn  14153  blpnf  14283  blininf  14307  blres  14317  xmetec  14320  metrest  14389  xmetxpbl  14391  cnbl0  14417  reopnap  14421  bl2ioo  14425  cncfmet  14462  limcdifap  14514