Theorem eleq1d 2239

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

Hypothesis

Ref	Expression
eleq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
eleq1d	|- ( ph -> ( A e. C <-> B e. C ) )

Proof of Theorem eleq1d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 |- ( ph -> A = B )
2		eleq1 2233	. 2 |- ( A = B -> ( A e. C <-> B e. C ) )
3	1, 2	syl 14	1 |- ( ph -> ( A e. C <-> B e. C ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   e. wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eleq12d  2241  eqeltrd  2247  eqneltrd  2266  eqneltrrd  2267  rspcimdv  2835  rspcimedv  2836  reuind  2935  sbcel2g  3070  sbccsb2g  3079  breq1  3992  breq2  3993  inex1g  4125  intexr  4136  pwexg  4166  prexg  4196  opelopabsb  4245  pofun  4297  seex  4320  uniex  4422  uniexg  4424  unexb  4427  abnexg  4431  reusv3  4445  rabxfrd  4454  onun2  4474  onsucelsucexmid  4514  ordsucunielexmid  4515  dcextest  4565  tfisi  4571  peano2  4579  seinxp  4682  opabid2  4742  opeliunxp2  4751  elrn2g  4801  opeldm  4814  opeldmg  4816  elreldm  4837  elrn2  4853  opelresg  4898  elsnres  4928  iss  4937  elimasng  4979  issref  4993  rnxpid  5045  unielrel  5138  dffun5r  5210  funopg  5232  brprcneu  5489  tz6.12f  5525  fvelrnb  5544  ssimaex  5557  dmfco  5564  fvmpt3  5575  mptfvex  5581  fvmptf  5588  respreima  5624  fvelrn  5627  ffnfvf  5655  ffvresb  5659  fmptco  5662  fmptcof  5663  fsn  5668  fressnfv  5683  fnex  5718  funfvima  5727  funfvima3  5729  f1mpt  5750  fliftfuns  5777  isoselem  5799  ovrspc2v  5879  ffnov  5957  fovcl  5958  ovmpos  5976  ov2gf  5977  ovg  5991  funimassov  6002  caovclg  6005  elovmpo  6050  off  6073  fnexALT  6090  fornex  6094  f1stres  6138  f2ndres  6139  xp1st  6144  xp2nd  6145  elxp6  6148  oprssdmm  6150  unielxp  6153  fmpox  6179  mpofvex  6182  opeliunxp2f  6217  dftpos4  6242  smoel  6279  tfrlem3-2d  6291  tfrlem8  6297  tfrlem9  6298  tfrlemibxssdm  6306  tfrlemi1  6311  tfrexlem  6313  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemaccex  6327  tfr1onlemres  6328  tfri1dALT  6330  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemaccex  6340  tfrcllemres  6341  tfrcl  6343  rdgtfr  6353  rdgon  6365  frecabex  6377  frecabcl  6378  frecfcllem  6383  frecsuclem  6385  nnacl  6459  nnmcl  6460  nnmordi  6495  nnaordex  6507  nnm00  6509  erexb  6538  qliftfuns  6597  ixpsnval  6679  elixp2  6680  resixp  6711  mptelixpg  6712  elixpsn  6713  fundmen  6784  fopwdom  6814  xpf1o  6822  dif1en  6857  diffitest  6865  diffifi  6872  inffiexmid  6884  unfiexmid  6895  unfidisj  6899  fiintim  6906  xpfi  6907  ssfirab  6911  fnfi  6914  iunfidisj  6923  snexxph  6927  fidcenumlemr  6932  elfi2  6949  ctssdccl  7088  isnumi  7159  cc2lem  7228  cc3  7230  addnidpig  7298  indpi  7304  dfplpq2  7316  addclnq  7337  mulclnq  7338  nnnq0lem1  7408  addclnq0  7413  mulclnq0  7414  nqpnq0nq  7415  distrnq0  7421  prloc  7453  prarloclemlo  7456  prarloclem3  7459  prarloclem5  7462  genpml  7479  genpmu  7480  addnqprl  7491  addnqpru  7492  mulnqprl  7530  mulnqpru  7531  ltexprlemell  7560  ltexprlemelu  7561  ltexprlemdisj  7568  ltexprlemloc  7569  ltexprlemrl  7572  ltexprlemru  7574  ltexpri  7575  recexprlemm  7586  recexprlemdisj  7592  recexprlemloc  7593  recexprlem1ssl  7595  recexprlem1ssu  7596  recexpr  7600  addclsr  7715  mulclsr  7716  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  suplocsr  7771  pitonn  7810  peano2nnnn  7815  axaddrcl  7827  axmulrcl  7829  peano5nnnn  7854  axpre-suploclemres  7863  negreb  8184  negf1o  8301  eqord1  8402  eqord2  8403  cju  8877  peano2nn  8890  nn1m1nn  8896  nnaddcl  8898  nnmulcl  8899  nnsub  8917  nndivtr  8920  un0addcl  9168  un0mulcl  9169  elnnnn0  9178  elz  9214  nnnegz  9215  znegclb  9245  zaddcllempos  9249  zaddcllemneg  9251  zaddcl  9252  nzadd  9264  zmulcl  9265  elz2  9283  zneo  9313  nneoor  9314  zeo  9317  peano5uzti  9320  zindd  9330  uzp1  9520  uzaddcl  9545  supinfneg  9554  infsupneg  9555  supminfex  9556  ublbneg  9572  eqreznegel  9573  negm  9574  qmulz  9582  qnegcl  9595  irradd  9605  irrmul  9606  fzrev2  10041  negqmod0  10287  frec2uzuzd  10358  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  frecuzrdgsuctlem  10379  iseqovex  10412  seq3val  10414  seqvalcd  10415  seq3-1  10416  seqf  10417  seq3p1  10418  seqovcd  10419  seqp1cd  10422  seq3clss  10423  monoord  10432  monoord2  10433  ser3mono  10434  seq3split  10435  seq3caopr3  10437  seq3caopr2  10438  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  iseqf1olemfvp  10453  seq3f1olemqsumkj  10454  seq3f1olemqsum  10456  seq3f1oleml  10459  seq3f1o  10460  seq3homo  10466  seq3z  10467  seq3distr  10469  ser3ge0  10473  expp1  10483  expcllem  10487  expcl2lemap  10488  m1expcl2  10498  facnn  10661  fac0  10662  fac1  10663  faccl  10669  facdiv  10672  facndiv  10673  bccmpl  10688  bcn2  10698  bccl  10701  focdmex  10721  fihasheqf1oi  10722  seq3coll  10777  shftlem  10780  shftf  10794  seq3shft  10802  cjval  10809  cjth  10810  remim  10824  uzin2  10951  caubnd2  11081  negfi  11191  xrmaxltsup  11221  clim  11244  clim2  11246  climshftlemg  11265  climcn1  11271  climcn2  11272  iserex  11302  climub  11307  climserle  11308  climcau  11310  serf0  11315  sumfct  11337  sumrbdclem  11340  fsum3cvg  11341  summodclem3  11343  summodclem2a  11344  zsumdc  11347  fsumgcl  11349  fsum3  11350  fsumf1o  11353  isumss  11354  isumss2  11356  fsum3cvg2  11357  fsum3ser  11360  fsumcl2lem  11361  fsumsplitf  11371  sumpr  11376  sumtp  11377  fsumm1  11379  fsum1p  11381  isummulc2  11389  fsum2dlemstep  11397  fisumcom2  11401  fsumshftm  11408  fisum0diag2  11410  fsummulc2  11411  fsumge1  11424  fsum00  11425  fsumabs  11428  telfsumo  11429  telfsumo2  11430  fsumparts  11433  fsumrelem  11434  fsumiun  11440  binomlem  11446  isumshft  11453  isum1p  11455  isumrpcl  11457  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemseq  11489  cvgratnnlemabsle  11490  cvgratnnlemfm  11492  cvgratnnlemrate  11493  cvgratnn  11494  cvgratz  11495  mertenslem2  11499  mertensabs  11500  clim2prod  11502  prodfap0  11508  prodfrecap  11509  prodfdivap  11510  prodrbdclem  11534  fproddccvg  11535  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  prodfct  11550  fprodf1o  11551  prodssdc  11552  fprodssdc  11553  fprodmul  11554  fprodm1  11561  fprod1p  11562  fprodm1s  11564  fprodp1s  11565  fprodcl2lem  11568  fprodabs  11579  fprod2dlemstep  11585  fprodcnv  11588  fprodcom2fi  11589  fprodrec  11592  fproddivapf  11594  fprodsplitf  11595  fprodsplit1f  11597  fprodle  11603  zeo3  11827  mulsucdiv2z  11844  zob  11850  nn0o1gt2  11864  nno  11865  nn0o  11866  infssuzex  11904  infssuzcldc  11906  zsupssdc  11909  uzwodc  11992  qnumdencl  12141  pcqcl  12260  pcxnn0cl  12264  pcxcl  12265  pcgcd1  12281  dvdsprmpweqle  12290  pcmpt  12295  pcmpt2  12296  pcmptdvds  12297  infpnlem2  12312  1arith  12319  elgz  12323  mul4sq  12346  znnen  12353  ennnfonelemj0  12356  ennnfonelemg  12358  ennnfonelemom  12363  ctinfom  12383  ctiunctlemu1st  12389  ctiunctlemu2nd  12390  ctiunctlemudc  12392  ctiunctlemfo  12394  ssnnctlemct  12401  infpn2  12411  isstruct2im  12426  isstruct2r  12427  mgmsscl  12615  mgm1  12624  mndpropd  12676  issubm  12695  0subm  12702  insubm  12703  mhmima  12706  uniopn  12793  inopn  12795  fiinopn  12796  iscld  12897  iuncld  12909  tgrest  12963  iscn  12991  cnpval  12992  iscnp  12993  tgcn  13002  ssidcn  13004  lmbrf  13009  cnpnei  13013  cnima  13014  cnconst2  13027  cnrest2  13030  cnptopresti  13032  cnptoprest  13033  lmres  13042  lmtopcnp  13044  txbasval  13061  tx1cn  13063  tx2cn  13064  txcnp  13065  txcnmpt  13067  txdis1cn  13072  txlm  13073  cnmpt11  13077  cnmpt12  13081  cnmpt21  13085  cnmpt22  13088  ishmeo  13098  hmeoopn  13105  hmeocld  13106  qtopbasss  13315  fsumcncntop  13350  expcncf  13386  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemdisj  13412  ivthinclemloc  13413  ivthinc  13415  ivthdec  13416  limccl  13422  ellimc3apf  13423  cnmptlimc  13437  limccoap  13441  2irrexpq  13688  2irrexpqap  13690  lgsval  13699  lgsval2lem  13705  lgsdir2lem4  13726  lgsdir2  13728  mul2sq  13746  2sqlem6  13750  bdinex1g  13936  bj-intexr  13943  bj-prexg  13946  bj-uniex  13952  bj-uniexg  13953  bdunexb  13955  bj-indsuc  13963  exmidsbthrlem  14054  qdencn  14059  iswomni0  14083