Theorem eqrdv 2162

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1340   = wceq 1342   ∈ wcel 2135

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 1434  ax-gen 1436  ax-17 1513  ax-ext 2146

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

This theorem is referenced by:  eqrdav  2163  csbcomg  3063  csbabg  3101  uneq1  3264  ineq1  3311  difin2  3379  difsn  3704  intmin4  3846  iunconstm  3868  iinconstm  3869  dfiun2g  3892  iindif2m  3927  iinin2m  3928  iunxsng  3935  iunxsngf  3937  iunpw  4452  opthprc  4649  inimasn  5015  dmsnopg  5069  dfco2a  5098  iotaeq  5155  fun11iun  5447  ssimaex  5541  unpreima  5604  respreima  5607  fconstfvm  5697  reldm  6146  rntpos  6216  frecsuclem  6365  iserd  6518  erth  6536  ecidg  6556  mapdm0  6620  map0e  6643  ixpiinm  6681  fifo  6936  ordiso2  6991  ctssdccl  7067  ctssdc  7069  genpassl  7456  genpassu  7457  1idprl  7522  1idpru  7523  sup3exmid  8843  eqreznegel  9543  iccid  9852  fzsplit2  9975  fzsn  9991  fzpr  10002  uzsplit  10017  fzoval  10073  frec2uzrand  10330  infssuzex  11867  discld  12677  restsn  12721  restdis  12725  cndis  12782  cnpdis  12783  tx1cn  12810  tx2cn  12811  blpnf  12941  blininf  12965  blres  12975  xmetec  12978  metrest  13047  xmetxpbl  13049  cnbl0  13075  reopnap  13079  bl2ioo  13083  cncfmet  13120  limcdifap  13172