Theorem eqrdv 2098

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1297   = wceq 1299   ∈ wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-17 1474  ax-ext 2082

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

This theorem is referenced by:  eqrdav  2099  csbcomg  2976  csbabg  3011  uneq1  3170  ineq1  3217  difin2  3285  difsn  3604  intmin4  3746  iunconstm  3768  iinconstm  3769  dfiun2g  3792  iindif2m  3827  iinin2m  3828  iunxsng  3835  iunxsngf  3837  iunpw  4339  opthprc  4528  inimasn  4892  dmsnopg  4946  dfco2a  4975  iotaeq  5032  fun11iun  5322  ssimaex  5414  unpreima  5477  respreima  5480  fconstfvm  5570  reldm  6014  rntpos  6084  frecsuclem  6233  iserd  6385  erth  6403  ecidg  6423  mapdm0  6487  map0e  6510  ixpiinm  6548  ordiso2  6835  ctssdclemr  6911  ctssdc  6912  genpassl  7233  genpassu  7234  1idprl  7299  1idpru  7300  sup3exmid  8573  eqreznegel  9256  iccid  9549  fzsplit2  9671  fzsn  9687  fzpr  9698  uzsplit  9713  fzoval  9766  frec2uzrand  10019  infssuzex  11437  discld  12087  restsn  12131  restdis  12135  cndis  12191  cnpdis  12192  tx1cn  12219  tx2cn  12220  blpnf  12328  blininf  12352  blres  12362  xmetec  12365  metrest  12434  cnbl0  12456  bl2ioo  12461  cncfmet  12492  limcdifap  12512