Theorem eleq2d 2275

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 2269	. 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 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleq12d  2276  eleqtrd  2284  neleqtrd  2303  neleqtrrd  2304  abeq2d  2318  nfceqdf  2347  drnfc1  2365  drnfc2  2366  sbcbid  3056  cbvcsbw  3097  cbvcsb  3098  sbcel1g  3112  csbeq2d  3118  csbie2g  3144  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  opeq1  3819  opeq2  3820  cbviun  3964  cbviin  3965  iinxsng  4001  iinxprg  4002  iunxsng  4003  iunxsngf  4005  cbvdisj  4031  disjnim  4035  disjiun  4039  mpteq12f  4124  axpweq  4215  rabxfrd  4516  onsucelsucexmid  4578  ordsucunielexmid  4579  0elsucexmid  4613  0nelelxp  4704  opeliunxp  4730  opeliunxp2  4818  iunxpf  4826  elrelimasn  5048  elimasng  5050  xpimasn  5131  ressn  5223  funfni  5376  fnbr  5378  fun11iun  5543  fvelrnb  5626  foelcdmi  5631  fvun1  5645  fvco2  5648  elfvmptrab1  5674  elfvmptrab  5675  elpreima  5699  dff3im  5725  resflem  5744  fmptco  5746  funfvima3  5818  foima2  5820  eluniimadm  5834  dff13  5837  f1eqcocnv  5860  isoini  5887  riotaeqdv  5900  mpoeq123dva  6006  cbvmpox  6023  ovelrn  6095  elovmpod  6144  elovmpo  6145  elovmporab  6146  elovmporab1w  6147  fmpox  6286  disjxp1  6322  opeliunxp2f  6324  mpoxopn0yelv  6325  mpoxopovel  6327  rbropapd  6328  rntpos  6343  smoel  6386  smoiso  6388  smoel2  6389  tfrlem9  6405  tfrlemisucaccv  6411  tfrlemiubacc  6416  tfrlemi14d  6419  tfri2d  6422  tfr1onlemubacc  6432  tfr1onlemres  6435  tfrcllemubacc  6445  tfrcllemres  6448  rdgon  6472  freceq1  6478  freceq2  6479  frec0g  6483  frecabcl  6485  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecsuc  6493  nnsucelsuc  6577  nnsucuniel  6581  nnmordi  6602  ereldm  6665  iinerm  6694  elmapg  6748  elpmg  6751  elixpsn  6822  ixpsnf1o  6823  pw2f1odclem  6931  phplem4  6952  phplem3g  6953  phplem4on  6964  exmidpw  7005  fiintim  7028  fidcenumlemrks  7055  fidcenumlemrk  7056  elfi  7073  ordiso2  7137  ctssdccl  7213  nnnninfeq  7230  cc2lem  7378  cc2  7379  cc3  7380  archnqq  7530  ltdfpr  7619  genpelxp  7624  genpelvl  7625  genpelvu  7626  addcanprleml  7727  addcanprlemu  7728  cauappcvgprlem1  7772  suplocexprlemell  7826  suplocexprlemmu  7831  suplocexprlemru  7832  suplocexprlemdisj  7833  suplocexprlemloc  7834  suplocexprlemub  7836  suplocexprlemlub  7837  cnm  7945  eluz1  9652  elixx1  10019  elioo2  10043  elfz1  10135  elfzp1  10194  fzpr  10199  fzsuc2  10201  fzrev3  10209  elfzp12  10221  fzm1  10222  fzoval  10270  elfzo  10271  fzodcel  10275  elfzom1b  10358  fzosplitsni  10364  nninfdcex  10380  zmodidfzo  10498  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  seqf1og  10666  bcval  10894  bcpasc  10911  fundm2domnop0  10990  wrdmap  11025  elovmpowrd  11035  ccatfvalfi  11048  elfzelfzccat  11056  ccatlid  11062  ccatass  11064  ccatrn  11065  swrdfv2  11116  ccatswrd  11123  swrdccat2  11124  shftfn  11135  shftval  11136  seq3shft  11149  iser3shft  11657  sumeq1  11666  summodclem3  11691  summodclem2a  11692  isumss  11702  fsumsplit  11718  sumsplitdc  11743  fsum2dlemstep  11745  fisumcom2  11749  fsumparts  11781  explecnv  11816  fprodsplitdc  11907  fprodsplit  11908  fprod2dlemstep  11933  fprodcom2fi  11937  eftlub  12001  divalgmod  12238  bitsval  12254  bitsp1e  12263  bitsp1o  12264  algfx  12374  eucalgcvga  12380  reumodprminv  12576  nnnn0modprm0  12578  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemf1  12789  ennnfonelemrn  12790  ctinfomlemom  12798  ctinfom  12799  ctiunctlemudc  12808  ctiunctlemf  12809  elrest  13078  ptex  13096  prdsbasmpt  13112  prdsbasmpt2  13120  pwselbasb  13125  imasaddfnlemg  13146  divsfval  13160  xpscf  13179  grpidvalg  13205  grpidpropdg  13206  grpidd  13215  issgrpd  13244  sgrppropd  13245  ismndd  13269  mndpropd  13272  imasmnd2  13284  imasmnd  13285  ismhm  13293  issubm  13304  imasgrp2  13446  imasgrp  13447  issubg  13509  subginv  13517  isnsg  13538  eqg0el  13565  quselbasg  13566  isghm  13579  resghm2b  13598  conjnmzb  13616  conjnsg  13617  ghmpropd  13619  imasabl  13672  isrngd  13715  rngpropd  13717  imasrng  13718  qusrng  13720  dfur2g  13724  srgidmlem  13740  issrgid  13743  ringcl  13775  isringid  13787  isringd  13803  imasring  13826  oppr0g  13843  oppr1g  13844  reldvdsrsrg  13854  dvdsrvald  13855  isunitd  13868  unitinvcl  13885  unitinvinv  13886  unitlinv  13888  unitrinv  13889  unitnegcl  13892  dvdsrpropdg  13909  isrhm  13920  isrim0  13923  rhmmul  13926  islring  13954  issubrng  13961  opprsubrngg  13973  issubrg  13983  resrhm2b  14011  rhmpropd  14016  rrgval  14024  aprval  14044  aprap  14048  islmod  14053  lmodprop2d  14110  islssm  14119  islssmg  14120  islssmd  14121  lssats2  14176  ellspsn  14179  ixpsnbasval  14228  islidlm  14241  isridlrng  14244  rspssp  14256  rnglidlmmgm  14258  2idlval  14264  isridl  14266  2idlelb  14267  quscrng  14295  rspsn  14296  zrhval  14379  zrhrhmb  14384  znf1o  14413  psrgrp  14447  mplelbascoe  14454  istopon  14485  eltg  14524  eltg2  14525  eltop  14541  eltop2  14542  eltop3  14543  iscld  14575  neiss2  14614  isnei  14616  lmfval  14664  cnfval  14666  iscn  14669  iscnp  14671  tgcn  14680  tgcnp  14681  lmbrf  14687  cnptopresti  14710  txbas  14730  eltx  14731  txdis  14749  txdis1cn  14750  hmeofvalg  14775  ishmeo  14776  ispsmet  14795  ismet  14816  isxmet  14817  elblps  14862  elbl  14863  elmopn  14918  neibl  14963  metrest  14978  txmetcnp  14990  txmetcn  14991  metcnpd  14992  elcncf  15045  ellimc3apf  15132  limcmpted  15135  cnlimcim  15143  cnlimc  15144  eldvap  15154  dvidsslem  15165  dviaddf  15177  dvimulf  15178  elply  15206  ply1termlem  15214  lgseisenlem3  15549  bj-sels  15850  2omap  15932  nninfall  15946  nninfsellemeq  15951