Theorem eqrdv 2227

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1393   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqrdav  2228  eqabdv  2358  csbcomg  3147  csbabg  3186  uneq1  3351  ineq1  3398  difin2  3466  difsn  3804  intmin4  3950  iunconstm  3972  iinconstm  3973  dfiun2g  3996  iindif2m  4032  iinin2m  4033  iunxsng  4040  iunxsngf  4042  iunpw  4570  opthprc  4769  inimasn  5145  dmsnopg  5199  dfco2a  5228  iotaeq  5286  fun11iun  5592  ssimaex  5694  unpreima  5759  respreima  5762  fconstfvm  5856  reldm  6330  rntpos  6401  frecsuclem  6550  iserd  6704  erth  6724  ecidg  6744  mapdm0  6808  map0e  6831  ixpiinm  6869  pw2f1odclem  6991  fifo  7143  ordiso2  7198  ctssdccl  7274  ctssdc  7276  finacn  7382  pw1if  7406  exmidapne  7442  acnccim  7454  genpassl  7707  genpassu  7708  1idprl  7773  1idpru  7774  sup3exmid  9100  eqreznegel  9805  iccid  10117  fzsplit2  10242  fzsn  10258  fzpr  10269  uzsplit  10284  fzoval  10340  infssuzex  10448  frec2uzrand  10622  bitsmod  12462  bitscmp  12464  divsfval  13356  mhmpropd  13494  eqgid  13758  ghmmhmb  13786  ghmpropd  13815  ablnsg  13866  opprsubgg  14042  opprunitd  14068  unitpropdg  14106  opprsubrngg  14169  subsubrng2  14173  subrngpropd  14174  subsubrg2  14204  subrgpropd  14211  rhmpropd  14212  lssats2  14372  lsspropdg  14389  discld  14804  restsn  14848  restdis  14852  cndis  14909  cnpdis  14910  tx1cn  14937  tx2cn  14938  blpnf  15068  blininf  15092  blres  15102  xmetec  15105  metrest  15174  xmetxpbl  15176  cnbl0  15202  reopnap  15214  bl2ioo  15218  cncfmet  15260  limcdifap  15330  gausslemma2dlem1a  15731  ushgredgedg  16018  ushgredgedgloop  16020