Theorem eqrdv 2168

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 1867	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfcleq 2164	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	2, 3	sylibr 133	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1346   = wceq 1348   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqrdav  2169  csbcomg  3072  csbabg  3110  uneq1  3274  ineq1  3321  difin2  3389  difsn  3717  intmin4  3859  iunconstm  3881  iinconstm  3882  dfiun2g  3905  iindif2m  3940  iinin2m  3941  iunxsng  3948  iunxsngf  3950  iunpw  4465  opthprc  4662  inimasn  5028  dmsnopg  5082  dfco2a  5111  iotaeq  5168  fun11iun  5463  ssimaex  5557  unpreima  5621  respreima  5624  fconstfvm  5714  reldm  6165  rntpos  6236  frecsuclem  6385  iserd  6539  erth  6557  ecidg  6577  mapdm0  6641  map0e  6664  ixpiinm  6702  fifo  6957  ordiso2  7012  ctssdccl  7088  ctssdc  7090  genpassl  7486  genpassu  7487  1idprl  7552  1idpru  7553  sup3exmid  8873  eqreznegel  9573  iccid  9882  fzsplit2  10006  fzsn  10022  fzpr  10033  uzsplit  10048  fzoval  10104  frec2uzrand  10361  infssuzex  11904  mhmpropd  12689  discld  12930  restsn  12974  restdis  12978  cndis  13035  cnpdis  13036  tx1cn  13063  tx2cn  13064  blpnf  13194  blininf  13218  blres  13228  xmetec  13231  metrest  13300  xmetxpbl  13302  cnbl0  13328  reopnap  13332  bl2ioo  13336  cncfmet  13373  limcdifap  13425