Theorem eleq2d 1538

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 1532	. 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 954   e. wcel 956

This theorem is referenced by:  eleq12d 1539  eleqtrd 1547  abeq2d 1569  sbcel1g 2009  sbcnestg 2034  hbopd 2493  cbviun 2584  iunxsn 2607  opprc1b 2791  hbimad 3404  elimasng 3419  eliniseg 3421  funfni 3580  fnbr 3582  fneu 3584  zfrep6 3606  hbfvd 3721  hbfvd2 3722  fnrnfv 3750  fvelrnb 3751  fvelimab 3756  eqfnfv 3788  dff2 3808  funfvima3 3845  eluniima 3858  f1fv 3865  isoini 3891  tfrlem9 3910  hboprd 3973  oprvalelrn 4030  oalimcl 4184  oaass 4185  omordi 4187  omordlim 4198  omlimcl 4199  odi 4200  oen0 4203  oeordi 4204  oeordsuc 4211  omsmolem 4246  elmapg 4323  phplem4 4497  php3 4501  inf3lemd 4592  inf3lem1 4593  inf3lem2 4594  inf3lem3 4595  trcl 4625  r1tr 4634  r1ord 4635  tz9.12lem3 4641  tz9.12 4642  rankval2 4650  rankid 4652  rankr1 4654  rankval3 4661  r1pwcl 4667  aceq3 4713  aceq5lem5 4719  aceq5 4720  kmlem2 4746  kmlem12 4756  kmlem13 4757  kmlem14 4758  zorn2lem1 4768  zorn2 4776  alephnbtwn 4848  cardaleph 4865  cardinfima 4871  genpelv 5083  genpprecl 5084  genpnnp 5088  hbnegd 5343  elioo1t 6323  elioo2t 6324  elioo3g 6325  elioc1t 6327  elico1t 6328  elicc1t 6329  icoshftf1olem 6351  eluz1t 6360  elfz1t 6410  elfz2t 6412  elfzlem 6413  fzrev3t 6454  seqzp1 6488  sumeq2 6931  dffsum 6944  elcncf 7208  acdcALT 7446  unbenlem 7455  infxpidmlem5 7507  eltgt 7568  eltg2t 7569  eltg3t 7576  eltopt 7579  eltop2t 7580  eltop3t 7581  iscld 7619  neiss2 7666  isnei 7668  lpfval 7692  lpval 7693  islp 7694  islp2 7697  islpi 7699  cnpfval 7707  iscn 7708  iscnp 7710  cnsscnp 7722  blfval 7787  elbl 7790  blrn 7793  isopn 7811  neibl 7829  metcnpf 7835  metcnconst 7837  metcnp 7839  metcn 7841  metdnsconst 7853  cncfmet 7857  lmfval 7877  caufval 7878  iscau 7888  lmss 7904  cmsss 7947  bcthlem15 7963  grpinvfval 8016  grpdivfval 8031  grplactf1o 8049  issubg 8068  nvelbl 8276  nvcni 8279  ipfval 8299  isssp 8330  sspn 8342  islno 8361  nvcnpi4 8368  isblo 8387  nmlno0 8400  ipdir 8446  ipass 8449  ubthlem1 8473  psref 8592  spwnex 8602  ocelt 9093  ocnelt 9109  pjoc2t 9210  shselt 9216  shsel2t 9224  shmods 9300  elspan 9404  h1de2ctlem 9417  elspansnt 9428  elspansn2t 9429  eigvalvalt 9763  elnlfnt 9791  eleigvect 9820  riesz3 9933  elghomlem2 10317  elgiso 10332  cayleythlem 10347  sppfi 10412  cdrci 10417  ishomeo 10440  hmph 10447  ist1 10494  iintlem1 10512  isded 10549  dedi 10550  iscat 10567  cati 10568  ishoma 10595  ishomc 10597  ishomd 10598  ismona 10615  ismonb 10616  imonclem 10619  isfuna 10628  isfunb 10629

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-cleq 1467  df-clel 1470

Copyright terms: Public domain