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  3311  ineq1  3358  difin2  3426  difsn  3760  intmin4  3903  iunconstm  3925  iinconstm  3926  dfiun2g  3949  iindif2m  3985  iinin2m  3986  iunxsng  3993  iunxsngf  3995  iunpw  4516  opthprc  4715  inimasn  5088  dmsnopg  5142  dfco2a  5171  iotaeq  5228  fun11iun  5526  ssimaex  5623  unpreima  5688  respreima  5691  fconstfvm  5781  reldm  6246  rntpos  6317  frecsuclem  6466  iserd  6620  erth  6640  ecidg  6660  mapdm0  6724  map0e  6747  ixpiinm  6785  pw2f1odclem  6897  fifo  7048  ordiso2  7103  ctssdccl  7179  ctssdc  7181  exmidapne  7330  genpassl  7594  genpassu  7595  1idprl  7660  1idpru  7661  sup3exmid  8987  eqreznegel  9691  iccid  10003  fzsplit2  10128  fzsn  10144  fzpr  10155  uzsplit  10170  fzoval  10226  infssuzex  10326  frec2uzrand  10500  bitsmod  12124  bitscmp  12126  divsfval  12997  mhmpropd  13124  eqgid  13382  ghmmhmb  13410  ghmpropd  13439  ablnsg  13490  opprsubgg  13666  opprunitd  13692  unitpropdg  13730  opprsubrngg  13793  subsubrng2  13797  subrngpropd  13798  subsubrg2  13828  subrgpropd  13835  rhmpropd  13836  lssats2  13996  lsspropdg  14013  discld  14398  restsn  14442  restdis  14446  cndis  14503  cnpdis  14504  tx1cn  14531  tx2cn  14532  blpnf  14662  blininf  14686  blres  14696  xmetec  14699  metrest  14768  xmetxpbl  14770  cnbl0  14796  reopnap  14808  bl2ioo  14812  cncfmet  14854  limcdifap  14924  gausslemma2dlem1a  15325