Theorem eqrdv 2204

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1371   = wceq 1373   ∈ wcel 2177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-17 1550  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199

This theorem is referenced by:  eqrdav  2205  eqabdv  2335  csbcomg  3120  csbabg  3159  uneq1  3324  ineq1  3371  difin2  3439  difsn  3776  intmin4  3919  iunconstm  3941  iinconstm  3942  dfiun2g  3965  iindif2m  4001  iinin2m  4002  iunxsng  4009  iunxsngf  4011  iunpw  4535  opthprc  4734  inimasn  5109  dmsnopg  5163  dfco2a  5192  iotaeq  5249  fun11iun  5555  ssimaex  5653  unpreima  5718  respreima  5721  fconstfvm  5815  reldm  6285  rntpos  6356  frecsuclem  6505  iserd  6659  erth  6679  ecidg  6699  mapdm0  6763  map0e  6786  ixpiinm  6824  pw2f1odclem  6946  fifo  7097  ordiso2  7152  ctssdccl  7228  ctssdc  7230  finacn  7332  pw1if  7356  exmidapne  7392  acnccim  7404  genpassl  7657  genpassu  7658  1idprl  7723  1idpru  7724  sup3exmid  9050  eqreznegel  9755  iccid  10067  fzsplit2  10192  fzsn  10208  fzpr  10219  uzsplit  10234  fzoval  10290  infssuzex  10398  frec2uzrand  10572  bitsmod  12342  bitscmp  12344  divsfval  13235  mhmpropd  13373  eqgid  13637  ghmmhmb  13665  ghmpropd  13694  ablnsg  13745  opprsubgg  13921  opprunitd  13947  unitpropdg  13985  opprsubrngg  14048  subsubrng2  14052  subrngpropd  14053  subsubrg2  14083  subrgpropd  14090  rhmpropd  14091  lssats2  14251  lsspropdg  14268  discld  14683  restsn  14727  restdis  14731  cndis  14788  cnpdis  14789  tx1cn  14816  tx2cn  14817  blpnf  14947  blininf  14971  blres  14981  xmetec  14984  metrest  15053  xmetxpbl  15055  cnbl0  15081  reopnap  15093  bl2ioo  15097  cncfmet  15139  limcdifap  15209  gausslemma2dlem1a  15610