Theorem eqrdv 2038

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

Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1241   = wceq 1243   ∈ wcel 1393

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 1336  ax-gen 1338  ax-17 1419  ax-ext 2022

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

This theorem is referenced by:  eqrdav  2039  csbcomg  2873  csbabg  2907  uneq1  3090  ineq1  3131  difin2  3199  difsn  3501  intmin4  3643  iunconstm  3665  iinconstm  3666  dfiun2g  3689  iindif2m  3724  iinin2m  3725  iunxsng  3732  iunpw  4211  opthprc  4391  inimasn  4741  dmsnopg  4792  dfco2a  4821  iotaeq  4875  fun11iun  5147  ssimaex  5234  unpreima  5292  respreima  5295  fconstfvm  5379  reldm  5812  rntpos  5872  frecsuclem3  5990  iserd  6132  erth  6150  ecidg  6170  ordiso2  6357  genpassl  6622  genpassu  6623  1idprl  6688  1idpru  6689  eqreznegel  8549  iccid  8794  fzsplit2  8914  fzsn  8929  fzpr  8939  uzsplit  8954  fzoval  9005  frec2uzrand  9191