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  6355  genpassl  6620  genpassu  6621  1idprl  6686  1idpru  6687  eqreznegel  8547  iccid  8792  fzsplit2  8912  fzsn  8927  fzpr  8937  uzsplit  8952  fzoval  9003  frec2uzrand  9165