Theorem eleq2d 2247

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 2241	. 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 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12d  2248  eleqtrd  2256  neleqtrd  2275  neleqtrrd  2276  abeq2d  2290  nfceqdf  2318  drnfc1  2336  drnfc2  2337  sbcbid  3020  cbvcsbw  3061  cbvcsb  3062  sbcel1g  3076  csbeq2d  3082  csbie2g  3107  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  opeq1  3777  opeq2  3778  cbviun  3922  cbviin  3923  iinxsng  3958  iinxprg  3959  iunxsng  3960  iunxsngf  3962  cbvdisj  3988  disjnim  3992  disjiun  3996  mpteq12f  4081  axpweq  4169  rabxfrd  4467  onsucelsucexmid  4527  ordsucunielexmid  4528  0elsucexmid  4562  0nelelxp  4653  opeliunxp  4679  opeliunxp2  4764  iunxpf  4772  elrelimasn  4991  elimasng  4993  xpimasn  5074  ressn  5166  funfni  5313  fnbr  5315  fun11iun  5479  fvelrnb  5560  foelcdmi  5565  fvun1  5579  fvco2  5582  elfvmptrab1  5607  elfvmptrab  5608  elpreima  5632  dff3im  5658  resflem  5677  fmptco  5679  funfvima3  5746  foima2  5748  eluniimadm  5761  dff13  5764  f1eqcocnv  5787  isoini  5814  riotaeqdv  5827  mpoeq123dva  5931  cbvmpox  5948  ovelrn  6018  elovmpo  6067  fmpox  6196  disjxp1  6232  opeliunxp2f  6234  mpoxopn0yelv  6235  mpoxopovel  6237  rbropapd  6238  rntpos  6253  smoel  6296  smoiso  6298  smoel2  6299  tfrlem9  6315  tfrlemisucaccv  6321  tfrlemiubacc  6326  tfrlemi14d  6329  tfri2d  6332  tfr1onlemubacc  6342  tfr1onlemres  6345  tfrcllemubacc  6355  tfrcllemres  6358  rdgon  6382  freceq1  6388  freceq2  6389  frec0g  6393  frecabcl  6395  freccllem  6398  frecfcllem  6400  frecsuclem  6402  frecsuc  6403  nnsucelsuc  6487  nnsucuniel  6491  nnmordi  6512  ereldm  6573  iinerm  6602  elmapg  6656  elpmg  6659  elixpsn  6730  ixpsnf1o  6731  phplem4  6850  phplem3g  6851  phplem4on  6862  exmidpw  6903  fiintim  6923  fidcenumlemrks  6947  fidcenumlemrk  6948  elfi  6965  ordiso2  7029  ctssdccl  7105  nnnninfeq  7121  cc2lem  7260  cc2  7261  cc3  7262  archnqq  7411  ltdfpr  7500  genpelxp  7505  genpelvl  7506  genpelvu  7507  addcanprleml  7608  addcanprlemu  7609  cauappcvgprlem1  7653  suplocexprlemell  7707  suplocexprlemmu  7712  suplocexprlemru  7713  suplocexprlemdisj  7714  suplocexprlemloc  7715  suplocexprlemub  7717  suplocexprlemlub  7718  cnm  7826  eluz1  9526  elixx1  9891  elioo2  9915  elfz1  10007  elfzp1  10065  fzpr  10070  fzsuc2  10072  fzrev3  10080  elfzp12  10092  fzm1  10093  fzoval  10141  elfzo  10142  fzodcel  10145  elfzom1b  10222  fzosplitsni  10228  zmodidfzo  10346  frecuzrdgtcl  10405  frecuzrdgfunlem  10412  bcval  10720  bcpasc  10737  shftfn  10824  shftval  10825  seq3shft  10838  iser3shft  11345  sumeq1  11354  summodclem3  11379  summodclem2a  11380  isumss  11390  fsumsplit  11406  sumsplitdc  11431  fsum2dlemstep  11433  fisumcom2  11437  fsumparts  11469  explecnv  11504  fprodsplitdc  11595  fprodsplit  11596  fprod2dlemstep  11621  fprodcom2fi  11625  eftlub  11689  divalgmod  11922  nninfdcex  11944  algfx  12042  eucalgcvga  12048  reumodprminv  12243  nnnn0modprm0  12245  ennnfonelemex  12405  ennnfonelemhom  12406  ennnfonelemf1  12409  ennnfonelemrn  12410  ctinfomlemom  12418  ctinfom  12419  ctiunctlemudc  12428  ctiunctlemf  12429  elrest  12681  grpidvalg  12722  grpidpropdg  12723  grpidd  12732  ismndd  12768  mndpropd  12771  ismhm  12781  issubm  12791  issubg  12960  subginv  12967  dfur2g  13045  srgidmlem  13061  issrgid  13064  ringcl  13096  isringid  13108  isringd  13120  oppr0g  13150  oppr1g  13151  reldvdsrsrg  13160  dvdsrvald  13161  isunitd  13174  unitinvcl  13191  unitinvinv  13192  unitlinv  13194  unitrinv  13195  unitnegcl  13198  dvdsrpropdg  13215  islring  13232  aprval  13239  aprap  13243  istopon  13293  eltg  13334  eltg2  13335  eltop  13351  eltop2  13352  eltop3  13353  iscld  13385  neiss2  13424  isnei  13426  lmfval  13474  cnfval  13476  iscn  13479  iscnp  13481  tgcn  13490  tgcnp  13491  lmbrf  13497  cnptopresti  13520  txbas  13540  eltx  13541  txdis  13559  txdis1cn  13560  hmeofvalg  13585  ishmeo  13586  ispsmet  13605  ismet  13626  isxmet  13627  elblps  13672  elbl  13673  elmopn  13728  neibl  13773  metrest  13788  txmetcnp  13800  txmetcn  13801  metcnpd  13802  elcncf  13842  ellimc3apf  13911  limcmpted  13914  cnlimcim  13922  cnlimc  13923  eldvap  13933  dviaddf  13951  dvimulf  13952  bj-sels  14437  nninfall  14529  nninfsellemeq  14534