Theorem eleq2d 2277

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 2271	. 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 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  eleq12d  2278  eleqtrd  2286  neleqtrd  2305  neleqtrrd  2306  abeq2d  2320  nfceqdf  2349  drnfc1  2367  drnfc2  2368  sbcbid  3063  cbvcsbw  3105  cbvcsb  3106  sbcel1g  3120  csbeq2d  3126  csbie2g  3152  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  opeq1  3833  opeq2  3834  cbviun  3978  cbviin  3979  iinxsng  4015  iinxprg  4016  iunxsng  4017  iunxsngf  4019  cbvdisj  4045  disjnim  4049  disjiun  4054  mpteq12f  4140  axpweq  4231  rabxfrd  4534  onsucelsucexmid  4596  ordsucunielexmid  4597  0elsucexmid  4631  0nelelxp  4722  opeliunxp  4748  opeliunxp2  4836  iunxpf  4844  elrelimasn  5067  elimasng  5069  xpimasn  5150  ressn  5242  funfni  5395  fnbr  5397  fun11iun  5565  fvelrnb  5649  foelcdmi  5654  fvun1  5668  fvco2  5671  elfvmptrab1  5697  elfvmptrab  5698  elpreima  5722  dff3im  5748  resflem  5767  fmptco  5769  funfvima3  5841  foima2  5843  eluniimadm  5857  dff13  5860  f1eqcocnv  5883  isoini  5910  riotaeqdv  5923  mpoeq123dva  6029  cbvmpox  6046  ovelrn  6118  elovmpod  6167  elovmpo  6168  elovmporab  6169  elovmporab1w  6170  fmpox  6309  disjxp1  6345  opeliunxp2f  6347  mpoxopn0yelv  6348  mpoxopovel  6350  rbropapd  6351  rntpos  6366  smoel  6409  smoiso  6411  smoel2  6412  tfrlem9  6428  tfrlemisucaccv  6434  tfrlemiubacc  6439  tfrlemi14d  6442  tfri2d  6445  tfr1onlemubacc  6455  tfr1onlemres  6458  tfrcllemubacc  6468  tfrcllemres  6471  rdgon  6495  freceq1  6501  freceq2  6502  frec0g  6506  frecabcl  6508  freccllem  6511  frecfcllem  6513  frecsuclem  6515  frecsuc  6516  nnsucelsuc  6600  nnsucuniel  6604  nnmordi  6625  ereldm  6688  iinerm  6717  elmapg  6771  elpmg  6774  elixpsn  6845  ixpsnf1o  6846  pw2f1odclem  6956  phplem4  6977  phplem3g  6978  phplem4on  6990  exmidpw  7031  fiintim  7054  fidcenumlemrks  7081  fidcenumlemrk  7082  elfi  7099  ordiso2  7163  ctssdccl  7239  nnnninfeq  7256  cc2lem  7413  cc2  7414  cc3  7415  archnqq  7565  ltdfpr  7654  genpelxp  7659  genpelvl  7660  genpelvu  7661  addcanprleml  7762  addcanprlemu  7763  cauappcvgprlem1  7807  suplocexprlemell  7861  suplocexprlemmu  7866  suplocexprlemru  7867  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemub  7871  suplocexprlemlub  7872  cnm  7980  eluz1  9687  elixx1  10054  elioo2  10078  elfz1  10170  elfzp1  10229  fzpr  10234  fzsuc2  10236  fzrev3  10244  elfzp12  10256  fzm1  10257  fzoval  10305  elfzo  10306  fzodcel  10310  elfzom1b  10395  fzosplitsni  10401  nninfdcex  10417  zmodidfzo  10535  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  seqf1og  10703  bcval  10931  bcpasc  10948  fundm2domnop0  11027  wrdmap  11062  elovmpowrd  11072  ccatfvalfi  11086  elfzelfzccat  11094  ccatlid  11100  ccatass  11102  ccatrn  11103  swrdfv2  11154  ccatswrd  11161  swrdccat2  11162  pfxfv  11175  pfxeq  11187  ccatpfx  11192  swrdswrd  11196  swrdpfx  11198  pfxpfx  11199  cats1un  11212  swrdccatfn  11215  swrdccatin1  11216  pfxccatin12lem4  11217  pfxccatin12lem1  11219  swrdccatin2  11220  pfxccatin12lem2c  11221  pfxccatin12lem2  11222  swrdccat3blem  11230  swrdccatin1d  11234  swrdccatin2d  11235  pfxccatin12d  11236  shftfn  11250  shftval  11251  seq3shft  11264  iser3shft  11772  sumeq1  11781  summodclem3  11806  summodclem2a  11807  isumss  11817  fsumsplit  11833  sumsplitdc  11858  fsum2dlemstep  11860  fisumcom2  11864  fsumparts  11896  explecnv  11931  fprodsplitdc  12022  fprodsplit  12023  fprod2dlemstep  12048  fprodcom2fi  12052  eftlub  12116  divalgmod  12353  bitsval  12369  bitsp1e  12378  bitsp1o  12379  algfx  12489  eucalgcvga  12495  reumodprminv  12691  nnnn0modprm0  12693  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemf1  12904  ennnfonelemrn  12905  ctinfomlemom  12913  ctinfom  12914  ctiunctlemudc  12923  ctiunctlemf  12924  elrest  13193  ptex  13211  prdsbasmpt  13227  prdsbasmpt2  13235  pwselbasb  13240  imasaddfnlemg  13261  divsfval  13275  xpscf  13294  grpidvalg  13320  grpidpropdg  13321  grpidd  13330  issgrpd  13359  sgrppropd  13360  ismndd  13384  mndpropd  13387  imasmnd2  13399  imasmnd  13400  ismhm  13408  issubm  13419  imasgrp2  13561  imasgrp  13562  issubg  13624  subginv  13632  isnsg  13653  eqg0el  13680  quselbasg  13681  isghm  13694  resghm2b  13713  conjnmzb  13731  conjnsg  13732  ghmpropd  13734  imasabl  13787  isrngd  13830  rngpropd  13832  imasrng  13833  qusrng  13835  dfur2g  13839  srgidmlem  13855  issrgid  13858  ringcl  13890  isringid  13902  isringd  13918  imasring  13941  oppr0g  13958  oppr1g  13959  reldvdsrsrg  13969  dvdsrvald  13970  isunitd  13983  unitinvcl  14000  unitinvinv  14001  unitlinv  14003  unitrinv  14004  unitnegcl  14007  dvdsrpropdg  14024  isrhm  14035  isrim0  14038  rhmmul  14041  islring  14069  issubrng  14076  opprsubrngg  14088  issubrg  14098  resrhm2b  14126  rhmpropd  14131  rrgval  14139  aprval  14159  aprap  14163  islmod  14168  lmodprop2d  14225  islssm  14234  islssmg  14235  islssmd  14236  lssats2  14291  ellspsn  14294  ixpsnbasval  14343  islidlm  14356  isridlrng  14359  rspssp  14371  rnglidlmmgm  14373  2idlval  14379  isridl  14381  2idlelb  14382  quscrng  14410  rspsn  14411  zrhval  14494  zrhrhmb  14499  znf1o  14528  psrgrp  14562  mplelbascoe  14569  istopon  14600  eltg  14639  eltg2  14640  eltop  14656  eltop2  14657  eltop3  14658  iscld  14690  neiss2  14729  isnei  14731  lmfval  14779  cnfval  14781  iscn  14784  iscnp  14786  tgcn  14795  tgcnp  14796  lmbrf  14802  cnptopresti  14825  txbas  14845  eltx  14846  txdis  14864  txdis1cn  14865  hmeofvalg  14890  ishmeo  14891  ispsmet  14910  ismet  14931  isxmet  14932  elblps  14977  elbl  14978  elmopn  15033  neibl  15078  metrest  15093  txmetcnp  15105  txmetcn  15106  metcnpd  15107  elcncf  15160  ellimc3apf  15247  limcmpted  15250  cnlimcim  15258  cnlimc  15259  eldvap  15269  dvidsslem  15280  dviaddf  15292  dvimulf  15293  elply  15321  ply1termlem  15329  lgseisenlem3  15664  edgiedgbg  15776  edgupgren  15845  upgredg  15848  bj-sels  16049  2omap  16132  pw1map  16134  nninfall  16148  nninfsellemeq  16153