Theorem eqrdv 2080

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

Syntax hints:   → wi 4   ↔ wb 103  ∀wal 1283   = wceq 1285   ∈ wcel 1434

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-17 1460  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075

This theorem is referenced by:  eqrdav  2081  csbcomg  2930  csbabg  2964  uneq1  3120  ineq1  3167  difin2  3233  difsn  3531  intmin4  3672  iunconstm  3694  iinconstm  3695  dfiun2g  3718  iindif2m  3753  iinin2m  3754  iunxsng  3761  iunpw  4237  opthprc  4417  inimasn  4771  dmsnopg  4822  dfco2a  4851  iotaeq  4905  fun11iun  5178  ssimaex  5266  unpreima  5324  respreima  5327  fconstfvm  5411  reldm  5843  rntpos  5906  frecsuclem  6055  iserd  6198  erth  6216  ecidg  6236  ordiso2  6505  genpassl  6776  genpassu  6777  1idprl  6842  1idpru  6843  eqreznegel  8780  iccid  9024  fzsplit2  9145  fzsn  9160  fzpr  9170  uzsplit  9185  fzoval  9235  frec2uzrand  9487  infssuzex  10489