Theorem eleq2d 2266

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)

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 2260	. 2 |- ( A = B -> ( C e. A <-> C e. B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C e. A <-> C e. B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   e. 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-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

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

This theorem is referenced by:  eleq12d  2267  eleqtrd  2275  neleqtrd  2294  neleqtrrd  2295  abeq2d  2309  nfceqdf  2338  drnfc1  2356  drnfc2  2357  sbcbid  3047  cbvcsbw  3088  cbvcsb  3089  sbcel1g  3103  csbeq2d  3109  csbie2g  3135  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  opeq1  3809  opeq2  3810  cbviun  3954  cbviin  3955  iinxsng  3991  iinxprg  3992  iunxsng  3993  iunxsngf  3995  cbvdisj  4021  disjnim  4025  disjiun  4029  mpteq12f  4114  axpweq  4205  rabxfrd  4505  onsucelsucexmid  4567  ordsucunielexmid  4568  0elsucexmid  4602  0nelelxp  4693  opeliunxp  4719  opeliunxp2  4807  iunxpf  4815  elrelimasn  5036  elimasng  5038  xpimasn  5119  ressn  5211  funfni  5361  fnbr  5363  fun11iun  5528  fvelrnb  5611  foelcdmi  5616  fvun1  5630  fvco2  5633  elfvmptrab1  5659  elfvmptrab  5660  elpreima  5684  dff3im  5710  resflem  5729  fmptco  5731  funfvima3  5799  foima2  5801  eluniimadm  5815  dff13  5818  f1eqcocnv  5841  isoini  5868  riotaeqdv  5881  mpoeq123dva  5987  cbvmpox  6004  ovelrn  6076  elovmpod  6125  elovmpo  6126  elovmporab  6127  elovmporab1w  6128  fmpox  6267  disjxp1  6303  opeliunxp2f  6305  mpoxopn0yelv  6306  mpoxopovel  6308  rbropapd  6309  rntpos  6324  smoel  6367  smoiso  6369  smoel2  6370  tfrlem9  6386  tfrlemisucaccv  6392  tfrlemiubacc  6397  tfrlemi14d  6400  tfri2d  6403  tfr1onlemubacc  6413  tfr1onlemres  6416  tfrcllemubacc  6426  tfrcllemres  6429  rdgon  6453  freceq1  6459  freceq2  6460  frec0g  6464  frecabcl  6466  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  nnsucelsuc  6558  nnsucuniel  6562  nnmordi  6583  ereldm  6646  iinerm  6675  elmapg  6729  elpmg  6732  elixpsn  6803  ixpsnf1o  6804  pw2f1odclem  6904  phplem4  6925  phplem3g  6926  phplem4on  6937  exmidpw  6978  fiintim  7001  fidcenumlemrks  7028  fidcenumlemrk  7029  elfi  7046  ordiso2  7110  ctssdccl  7186  nnnninfeq  7203  cc2lem  7349  cc2  7350  cc3  7351  archnqq  7501  ltdfpr  7590  genpelxp  7595  genpelvl  7596  genpelvu  7597  addcanprleml  7698  addcanprlemu  7699  cauappcvgprlem1  7743  suplocexprlemell  7797  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  suplocexprlemlub  7808  cnm  7916  eluz1  9622  elixx1  9989  elioo2  10013  elfz1  10105  elfzp1  10164  fzpr  10169  fzsuc2  10171  fzrev3  10179  elfzp12  10191  fzm1  10192  fzoval  10240  elfzo  10241  fzodcel  10245  elfzom1b  10322  fzosplitsni  10328  nninfdcex  10344  zmodidfzo  10462  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  seqf1og  10630  bcval  10858  bcpasc  10875  wrdmap  10983  elovmpowrd  10993  shftfn  11006  shftval  11007  seq3shft  11020  iser3shft  11528  sumeq1  11537  summodclem3  11562  summodclem2a  11563  isumss  11573  fsumsplit  11589  sumsplitdc  11614  fsum2dlemstep  11616  fisumcom2  11620  fsumparts  11652  explecnv  11687  fprodsplitdc  11778  fprodsplit  11779  fprod2dlemstep  11804  fprodcom2fi  11808  eftlub  11872  divalgmod  12109  bitsval  12125  bitsp1e  12134  bitsp1o  12135  algfx  12245  eucalgcvga  12251  reumodprminv  12447  nnnn0modprm0  12449  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemf1  12660  ennnfonelemrn  12661  ctinfomlemom  12669  ctinfom  12670  ctiunctlemudc  12679  ctiunctlemf  12680  elrest  12948  ptex  12966  prdsbasmpt  12982  prdsbasmpt2  12990  pwselbasb  12995  imasaddfnlemg  13016  divsfval  13030  xpscf  13049  grpidvalg  13075  grpidpropdg  13076  grpidd  13085  issgrpd  13114  sgrppropd  13115  ismndd  13139  mndpropd  13142  imasmnd2  13154  imasmnd  13155  ismhm  13163  issubm  13174  imasgrp2  13316  imasgrp  13317  issubg  13379  subginv  13387  isnsg  13408  eqg0el  13435  quselbasg  13436  isghm  13449  resghm2b  13468  conjnmzb  13486  conjnsg  13487  ghmpropd  13489  imasabl  13542  isrngd  13585  rngpropd  13587  imasrng  13588  qusrng  13590  dfur2g  13594  srgidmlem  13610  issrgid  13613  ringcl  13645  isringid  13657  isringd  13673  imasring  13696  oppr0g  13713  oppr1g  13714  reldvdsrsrg  13724  dvdsrvald  13725  isunitd  13738  unitinvcl  13755  unitinvinv  13756  unitlinv  13758  unitrinv  13759  unitnegcl  13762  dvdsrpropdg  13779  isrhm  13790  isrim0  13793  rhmmul  13796  islring  13824  issubrng  13831  opprsubrngg  13843  issubrg  13853  resrhm2b  13881  rhmpropd  13886  rrgval  13894  aprval  13914  aprap  13918  islmod  13923  lmodprop2d  13980  islssm  13989  islssmg  13990  islssmd  13991  lssats2  14046  ellspsn  14049  ixpsnbasval  14098  islidlm  14111  isridlrng  14114  rspssp  14126  rnglidlmmgm  14128  2idlval  14134  isridl  14136  2idlelb  14137  quscrng  14165  rspsn  14166  zrhval  14249  zrhrhmb  14254  znf1o  14283  psrgrp  14313  istopon  14333  eltg  14372  eltg2  14373  eltop  14389  eltop2  14390  eltop3  14391  iscld  14423  neiss2  14462  isnei  14464  lmfval  14512  cnfval  14514  iscn  14517  iscnp  14519  tgcn  14528  tgcnp  14529  lmbrf  14535  cnptopresti  14558  txbas  14578  eltx  14579  txdis  14597  txdis1cn  14598  hmeofvalg  14623  ishmeo  14624  ispsmet  14643  ismet  14664  isxmet  14665  elblps  14710  elbl  14711  elmopn  14766  neibl  14811  metrest  14826  txmetcnp  14838  txmetcn  14839  metcnpd  14840  elcncf  14893  ellimc3apf  14980  limcmpted  14983  cnlimcim  14991  cnlimc  14992  eldvap  15002  dvidsslem  15013  dviaddf  15025  dvimulf  15026  elply  15054  ply1termlem  15062  lgseisenlem3  15397  bj-sels  15644  2omap  15726  nninfall  15740  nninfsellemeq  15745