Theorem eqrdv 2229

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

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

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 1495  ax-gen 1497  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqrdav  2230  eqabdv  2360  csbcomg  3150  csbabg  3189  uneq1  3354  ineq1  3401  difin2  3469  difsn  3810  intmin4  3956  iunconstm  3978  iinconstm  3979  dfiun2g  4002  iindif2m  4038  iinin2m  4039  iunxsng  4046  iunxsngf  4048  iunpw  4577  opthprc  4777  inimasn  5154  dmsnopg  5208  dfco2a  5237  iotaeq  5295  fun11iun  5605  ssimaex  5708  unpreima  5773  respreima  5776  fconstfvm  5873  reldm  6352  rntpos  6426  frecsuclem  6575  iserd  6731  erth  6751  ecidg  6771  mapdm0  6835  map0e  6858  ixpiinm  6896  pw2f1odclem  7023  fifo  7182  ordiso2  7237  ctssdccl  7313  ctssdc  7315  finacn  7422  pw1if  7446  exmidapne  7482  acnccim  7494  genpassl  7747  genpassu  7748  1idprl  7813  1idpru  7814  sup3exmid  9140  eqreznegel  9851  iccid  10163  fzsplit2  10288  fzsn  10304  fzpr  10315  uzsplit  10330  fzoval  10386  infssuzex  10497  frec2uzrand  10671  bitsmod  12538  bitscmp  12540  divsfval  13432  mhmpropd  13570  eqgid  13834  ghmmhmb  13862  ghmpropd  13891  ablnsg  13942  opprsubgg  14119  opprunitd  14146  unitpropdg  14184  opprsubrngg  14247  subsubrng2  14251  subrngpropd  14252  subsubrg2  14282  subrgpropd  14289  rhmpropd  14290  lssats2  14450  lsspropdg  14467  discld  14887  restsn  14931  restdis  14935  cndis  14992  cnpdis  14993  tx1cn  15020  tx2cn  15021  blpnf  15151  blininf  15175  blres  15185  xmetec  15188  metrest  15257  xmetxpbl  15259  cnbl0  15285  reopnap  15297  bl2ioo  15301  cncfmet  15343  limcdifap  15413  gausslemma2dlem1a  15814  ushgredgedg  16104  ushgredgedgloop  16106  clwwlknun  16319  eupth2lemsfi  16356