Theorem eqrdv 2194

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1362   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqrdav  2195  eqabdv  2325  csbcomg  3107  csbabg  3146  uneq1  3310  ineq1  3357  difin2  3425  difsn  3759  intmin4  3902  iunconstm  3924  iinconstm  3925  dfiun2g  3948  iindif2m  3984  iinin2m  3985  iunxsng  3992  iunxsngf  3994  iunpw  4515  opthprc  4714  inimasn  5087  dmsnopg  5141  dfco2a  5170  iotaeq  5227  fun11iun  5525  ssimaex  5622  unpreima  5687  respreima  5690  fconstfvm  5780  reldm  6244  rntpos  6315  frecsuclem  6464  iserd  6618  erth  6638  ecidg  6658  mapdm0  6722  map0e  6745  ixpiinm  6783  pw2f1odclem  6895  fifo  7046  ordiso2  7101  ctssdccl  7177  ctssdc  7179  exmidapne  7327  genpassl  7591  genpassu  7592  1idprl  7657  1idpru  7658  sup3exmid  8984  eqreznegel  9688  iccid  10000  fzsplit2  10125  fzsn  10141  fzpr  10152  uzsplit  10167  fzoval  10223  infssuzex  10323  frec2uzrand  10497  divsfval  12971  mhmpropd  13098  eqgid  13356  ghmmhmb  13384  ghmpropd  13413  ablnsg  13464  opprsubgg  13640  opprunitd  13666  unitpropdg  13704  opprsubrngg  13767  subsubrng2  13771  subrngpropd  13772  subsubrg2  13802  subrgpropd  13809  rhmpropd  13810  lssats2  13970  lsspropdg  13987  discld  14372  restsn  14416  restdis  14420  cndis  14477  cnpdis  14478  tx1cn  14505  tx2cn  14506  blpnf  14636  blininf  14660  blres  14670  xmetec  14673  metrest  14742  xmetxpbl  14744  cnbl0  14770  reopnap  14782  bl2ioo  14786  cncfmet  14828  limcdifap  14898  gausslemma2dlem1a  15299