Theorem eleq2d 1541

Description: Deduction from equality to equivalence of membership.

Hypothesis

Ref	Expression
eleq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
eleq2d	|- (ph -> (C e. A <-> C e. B))

Proof of Theorem eleq2d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 |- (ph -> A = B)
2		eleq2 1535	. 2 |- (A = B -> (C e. A <-> C e. B))
3	1, 2	syl 10	1 |- (ph -> (C e. A <-> C e. B))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956   e. wcel 958

This theorem is referenced by:  eleq12d 1542  eleqtrd 1550  abeq2d 1572  sbcel1g 2013  sbcnestg 2038  hbopd 2497  cbviun 2589  iunxsn 2612  opprc1b 2796  hbimad 3412  elimasng 3427  eliniseg 3429  funfni 3588  fnbr 3590  fneu 3592  zfrep6 3614  hbfvd 3730  hbfvd2 3731  fnrnfv 3759  fvelrnb 3760  fvelimab 3765  eqfnfv 3797  dff2 3817  funfvima3 3854  eluniima 3867  f1fv 3874  isoini 3900  tfrlem9 3919  hboprd 3982  oprvalelrn 4039  oalimcl 4194  oaass 4195  omordi 4197  omordlim 4208  omlimcl 4209  odi 4210  oen0 4213  oeordi 4214  oeordsuc 4221  omsmolem 4256  elmapg 4333  phplem4 4511  php3 4515  php3OLD 4516  inf3lemd 4612  inf3lem1 4613  inf3lem2 4614  inf3lem3 4615  trcl 4645  r1tr 4654  r1ord 4655  tz9.12lem3 4661  tz9.12 4662  rankval2 4670  rankid 4672  rankr1 4674  rankval3 4681  r1pwcl 4687  aceq3 4733  aceq5lem5 4739  aceq5 4740  kmlem2 4766  kmlem12 4776  kmlem13 4777  kmlem14 4778  zorn2lem1 4788  zorn2 4796  alephnbtwn 4868  cardaleph 4885  cardinfima 4891  genpelv 5103  genpprecl 5104  genpnnp 5108  hbnegd 5363  elioo1t 6378  elioo2t 6379  elioo3g 6380  elioc1t 6381  elico1t 6382  elicc1t 6383  icoshftf1olem 6410  eluz1t 6420  elfz1t 6470  elfz2t 6472  elfzlem 6473  fzrev3t 6514  seqzp1 6548  sumeq2 6985  dffsum 6998  elcncf 7265  acdcALT 7496  unbenlem 7504  infxpidmlem5 7556  eltgt 7618  eltg2t 7619  eltg3t 7626  eltopt 7629  eltop2t 7630  eltop3t 7631  iscld 7669  neiss2 7716  isnei 7718  lpfval 7742  lpval 7743  islp 7744  islp2 7747  islpi 7749  cnpfval 7757  iscn 7758  iscnp 7760  cnsscnp 7772  blfval 7835  elbl 7838  blrn 7841  isopn 7859  neibl 7877  metcnpf 7883  metcnconst 7885  metcnp 7887  metcn 7889  metdnsconst 7901  cncfmet 7905  lmfval 7925  caufval 7926  iscau 7936  lmss 7953  cmsss 7997  bcthlem15 8013  grpinvfval 8066  grpdivfval 8081  grplactf1o 8098  issubg 8116  nvelbl 8325  nvcnpf 8328  nvcni 8329  nvcni2 8330  ipfval 8352  isssp 8383  sspn 8395  islno 8414  nvcnpi3 8422  nvcnpi4 8423  isblo 8442  nmlno0 8455  ipdir 8502  ipass 8505  ubthlem1 8529  psref 8649  spwnex 8661  spwpr3OLD 8662  ocelt 9154  ocnelt 9170  pjoc2t 9272  shselt 9278  shsel2t 9286  shmods 9362  elspan 9466  h1de2ctlem 9478  elspansnt 9489  elspansn2t 9490  eigvalvalt 9823  elnlfnt 9852  eleigvect 9881  riesz3 9995  elghomlem2 10383  elgiso 10398  cayleythlem 10413  sppfi 10486  sppfiOLD 10487  cdrci 10494  ishomeo 10517  hmph 10524  sfvlimOLD 10606  limfillem2OLD 10608  plimfilOLD 10609  ist1 10614  iintlem1 10632  isded 10669  dedi 10670  iscat 10687  cati 10688  ishoma 10715  ishomc 10717  ishomd 10718  ismona 10737  ismonb 10738  imonclem 10741  isepia 10747  isepib 10748  isfuna 10754  isfunb 10755

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain