Theorem eqrdv 2163

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1341   = wceq 1343   ∈ wcel 2136

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 1435  ax-gen 1437  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  eqrdav  2164  csbcomg  3068  csbabg  3106  uneq1  3269  ineq1  3316  difin2  3384  difsn  3710  intmin4  3852  iunconstm  3874  iinconstm  3875  dfiun2g  3898  iindif2m  3933  iinin2m  3934  iunxsng  3941  iunxsngf  3943  iunpw  4458  opthprc  4655  inimasn  5021  dmsnopg  5075  dfco2a  5104  iotaeq  5161  fun11iun  5453  ssimaex  5547  unpreima  5610  respreima  5613  fconstfvm  5703  reldm  6154  rntpos  6225  frecsuclem  6374  iserd  6527  erth  6545  ecidg  6565  mapdm0  6629  map0e  6652  ixpiinm  6690  fifo  6945  ordiso2  7000  ctssdccl  7076  ctssdc  7078  genpassl  7465  genpassu  7466  1idprl  7531  1idpru  7532  sup3exmid  8852  eqreznegel  9552  iccid  9861  fzsplit2  9985  fzsn  10001  fzpr  10012  uzsplit  10027  fzoval  10083  frec2uzrand  10340  infssuzex  11882  discld  12786  restsn  12830  restdis  12834  cndis  12891  cnpdis  12892  tx1cn  12919  tx2cn  12920  blpnf  13050  blininf  13074  blres  13084  xmetec  13087  metrest  13156  xmetxpbl  13158  cnbl0  13184  reopnap  13188  bl2ioo  13192  cncfmet  13229  limcdifap  13281