Theorem eleq1d 2307

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleq12d  2309  eqeltrd  2315  eqneltrd  2334  eqneltrrd  2335  rspcimdv  2930  rspcimedv  2931  reuind  3031  sbcel2g  3168  sbccsb2g  3177  breq1  4134  breq2  4135  inex1g  4271  intexr  4288  pwexg  4319  prexg  4351  opelopabsb  4404  pofun  4459  seex  4482  uniex  4585  uniexg  4587  unexb  4590  abnexg  4594  reusv3  4608  rabxfrd  4617  onun2  4639  onsucelsucexmid  4679  ordsucunielexmid  4680  dcextest  4730  tfisi  4736  peano2  4744  seinxp  4848  opabid2  4913  opeliunxp2  4922  elrn2g  4972  opeldm  4986  opeldmg  4988  elreldm  5010  elrn2  5026  opelresg  5072  elsnres  5102  iss  5112  xpexcnvm  5145  elimasng  5158  issref  5173  rnxpid  5225  unielrel  5318  dffun5r  5392  funopg  5414  brprcneu  5691  tz6.12f  5727  fvelrnb  5753  ssimaex  5767  dmfco  5776  fvmpt3  5787  mptfvex  5794  fvmptf  5801  respreima  5839  fvelrn  5842  ffnfvf  5870  ffvresb  5874  fmptco  5877  fmptcof  5878  fsn  5883  fsn2g  5886  fressnfv  5905  fnex  5940  funfvima  5953  funfvima3  5955  f1mpt  5980  fliftfuns  6007  isoselem  6029  ovrspc2v  6114  ffnov  6195  fovcld  6196  ovmpos  6215  ov2gf  6216  ovg  6231  funimassov  6242  caovclg  6245  elovmpo  6291  off  6319  caofdig  6340  fnexALT  6344  focdmex  6348  f1stres  6397  f2ndres  6398  xp1st  6403  xp2nd  6404  elxp6  6407  oprssdmm  6409  unielxp  6412  fmpox  6440  mpofvex  6445  elmpom  6478  suppofss1dcl  6508  suppofss2dcl  6509  opeliunxp2f  6513  dftpos4  6538  smoel  6575  tfrlem3-2d  6587  tfrlem8  6593  tfrlem9  6594  tfrlemibxssdm  6602  tfrlemi1  6607  tfrexlem  6609  tfr1onlemsucfn  6615  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemaccex  6623  tfr1onlemres  6624  tfri1dALT  6626  tfrcllemsucfn  6628  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemaccex  6636  tfrcllemres  6637  tfrcl  6639  rdgtfr  6649  rdgon  6661  frecabex  6673  frecabcl  6674  frecfcllem  6679  frecsuclem  6681  nnacl  6757  nnmcl  6758  nnmordi  6793  nnaordex  6805  nnm00  6807  erexb  6836  qliftfuns  6897  ixpsnval  6987  elixp2  6988  resixp  7019  mptelixpg  7020  elixpsn  7021  fundmen  7098  fopwdom  7140  xpf1o  7148  dif1en  7187  diffitest  7195  diffifi  7202  inffiexmid  7217  unfiexmid  7229  unfidisj  7233  prfidceq  7239  fiintim  7242  xpfi  7243  ssfirab  7248  fnfi  7254  iunfidisj  7264  mapfi  7265  relresfin  7268  snexxph  7272  fidcenumlemr  7277  isfsupp  7294  ffsuppbi  7305  elfi2  7311  ctssdccl  7457  isnumi  7533  cc2lem  7638  cc3  7640  addnidpig  7709  indpi  7715  dfplpq2  7727  addclnq  7748  mulclnq  7749  nnnq0lem1  7819  addclnq0  7824  mulclnq0  7825  nqpnq0nq  7826  distrnq0  7832  prloc  7864  prarloclemlo  7867  prarloclem3  7870  prarloclem5  7873  genpml  7890  genpmu  7891  addnqprl  7902  addnqpru  7903  mulnqprl  7941  mulnqpru  7942  ltexprlemell  7971  ltexprlemelu  7972  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  ltexpri  7986  recexprlemm  7997  recexprlemdisj  8003  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  recexpr  8011  addclsr  8126  mulclsr  8127  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  suplocsr  8182  pitonn  8221  peano2nnnn  8226  axaddrcl  8238  axmulrcl  8240  peano5nnnn  8265  axpre-suploclemres  8274  negreb  8598  negf1o  8716  eqord1  8818  eqord2  8819  cju  9299  indfval  9308  peano2nn  9325  nn1m1nn  9331  nnaddcl  9333  nnmulcl  9334  nnsub  9352  nndivtr  9355  un0addcl  9607  un0mulcl  9608  elnnnn0  9617  fcdmnn0fsuppg  9629  elz  9657  nnnegz  9658  znegclb  9688  zaddcllempos  9692  zaddcllemneg  9694  zaddcl  9695  nzadd  9708  zmulcl  9709  elz2  9727  zneo  9758  nneoor  9759  zeo  9762  peano5uzti  9765  zindd  9775  uzp1  9972  uzaddcl  10002  supinfneg  10011  infsupneg  10012  supminfex  10013  ublbneg  10029  eqreznegel  10030  negm  10031  qmulz  10039  qnegcl  10052  irradd  10062  irrmul  10064  fzsplit3  10475  fzspl  10493  fzrev2  10509  infssuzex  10683  infssuzcldc  10685  zsupssdc  10690  negqmod0  10789  frec2uzuzd  10860  frecuzrdgrrn  10866  frec2uzrdg  10867  frecuzrdgrcl  10868  frecuzrdgsuc  10872  frecuzrdgrclt  10873  frecuzrdgg  10874  frecuzrdgsuctlem  10881  xnn0nnen  10895  iseqovex  10916  seq3val  10918  seqvalcd  10919  seq3-1  10920  seqf  10922  seq3p1  10923  seqovcd  10925  seqp1cd  10928  seq3clss  10929  monoord  10943  monoord2  10944  ser3mono  10945  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seq3caopr2  10951  seqcaopr2g  10952  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  iseqf1olemfvp  10968  seq3f1olemqsumkj  10969  seq3f1olemqsum  10971  seq3f1oleml  10974  seq3f1o  10975  seqf1og  10979  seq3homo  10985  seq3z  10986  seqhomog  10988  seqfeq4g  10989  seq3distr  10990  ser3ge0  10994  expp1  11004  expcllem  11008  expcl2lemap  11009  m1expcl2  11019  facnn  11187  fac0  11188  fac1  11189  faccl  11195  facdiv  11198  facndiv  11199  bccmpl  11214  bcn2  11224  bccl  11227  fihasheqf1oi  11248  hashf1lem2  11308  seq3coll  11316  ccatalpha  11403  reuccatpfxs1lem  11540  reuccatpfxs1  11541  shftlem  11603  shftf  11617  seq3shft  11625  cjval  11632  cjth  11633  remim  11647  uzin2  11775  caubnd2  11906  negfi  12017  xrmaxltsup  12049  clim  12072  clim2  12074  climshftlemg  12093  climcn1  12099  climcn2  12100  iserex  12130  climub  12135  climserle  12136  climcau  12138  serf0  12143  sumfct  12165  sumrbdclem  12169  fsum3cvg  12170  summodclem3  12172  summodclem2a  12173  zsumdc  12176  fsumgcl  12178  fsum3  12179  fsumf1o  12182  isumss  12183  isumss2  12185  fsum3cvg2  12186  fsum3ser  12189  fsumcl2lem  12190  fsumsplitf  12200  sumpr  12205  sumtp  12206  fsumm1  12208  fsum1p  12210  isummulc2  12218  fsum2dlemstep  12226  fisumcom2  12230  fsumshftm  12237  fisum0diag2  12239  fsummulc2  12240  fsumge1  12253  fsum00  12254  fsumabs  12257  telfsumo  12258  telfsumo2  12259  fsumparts  12262  fsumrelem  12263  fsumiun  12269  binomlem  12275  isumshft  12282  isum1p  12284  isumrpcl  12286  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemseq  12318  cvgratnnlemabsle  12319  cvgratnnlemfm  12321  cvgratnnlemrate  12322  cvgratnn  12323  cvgratz  12324  mertenslem2  12328  mertensabs  12329  clim2prod  12331  prodfap0  12337  prodfrecap  12338  prodfdivap  12339  prodrbdclem  12363  fproddccvg  12364  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  prodfct  12379  fprodf1o  12380  prodssdc  12381  fprodssdc  12382  fprodmul  12383  fprodm1  12390  fprod1p  12391  fprodm1s  12393  fprodp1s  12394  fprodcl2lem  12397  fprodabs  12408  fprod2dlemstep  12414  fprodcnv  12417  fprodcom2fi  12418  fprodrec  12421  fproddivapf  12423  fprodsplitf  12424  fprodsplit1f  12426  fprodle  12432  zeo3  12660  mulsucdiv2z  12677  zob  12683  nn0o1gt2  12697  nno  12698  nn0o  12699  uzwodc  12839  qnumdencl  12992  pcqcl  13114  pcxnn0cl  13118  pcxcl  13119  pcgcd1  13136  dvdsprmpweqle  13145  pcmpt  13151  pcmpt2  13152  pcmptdvds  13153  infpnlem2  13168  1arith  13175  elgz  13179  mul4sq  13202  4sqlem13m  13211  4sqlem17  13215  4sqlem18  13216  4sqlem19  13217  ballotfilemsdom  13313  ballotfilemrv  13321  ballotfilemrv1  13322  ballotfilemrv2  13323  ballotfilem1ri  13336  znnen  13347  ennnfonelemj0  13350  ennnfonelemg  13352  ennnfonelemom  13357  ctinfom  13377  ctiunctlemu1st  13383  ctiunctlemu2nd  13384  ctiunctlemudc  13386  ctiunctlemfo  13388  ssnnctlemct  13395  infpn2  13405  isstruct2im  13420  isstruct2r  13421  imasaddfnlemg  13694  ercpbl  13711  xpsfrnel2  13726  mgmsscl  13740  mgm1  13749  sgrppropd  13787  mndpropd  13812  issubm  13838  0subm  13850  insubm  13851  mhmima  13857  mulgsubcl  13998  issubg  14035  subgex  14038  issubg2m  14051  issubg4m  14055  0subg  14061  isnsg  14064  isnsg2  14065  nsgbi  14066  isnsg3  14069  elnmz  14070  nmzbi  14071  nmzsubg  14072  nmznsg  14075  releqgg  14082  eqgex  14083  eqgval  14085  eqgid  14088  ghmrn  14119  ghmnsgima  14130  eqgabl  14224  ablnsg  14228  gzsummhm2  14236  gsumvalfi  14242  gsumclfi  14249  gsummptfidmadd  14251  gsumsubmclfi  14253  gsummptfidmsplit  14254  gsummhm2fi  14265  idjusnfi  14270  gsum2dfilem2  14272  gsumcom2fi  14275  isrng  14340  issrg  14376  srgfcl  14384  isring  14411  iscrng  14414  dvdsrd  14510  unitsubm  14535  isrim0  14577  issubrng  14616  subrngringnsg  14622  issubrng2  14627  opprsubrngg  14628  issubrg  14638  subrgsubm  14651  subrgugrp  14657  issubrg2  14658  issubrg3  14664  subrgpropd  14670  aprval  14700  aprunit  14701  aprsym  14705  opprdrng  14729  islmod  14736  lmodlema  14737  islmodd  14738  lmodprop2d  14794  rmodislmodlem  14796  rmodislmod  14797  lsssetm  14802  islssmd  14805  lssclg  14810  lsslss  14827  lsspropdg  14877  islidlm  14925  rnglidlmcl  14926  isridlrng  14928  rnglidlmmgm  14942  isridl  14950  gsumfsum  15032  psrbag  15162  psr1clfi  15198  uniopn  15227  inopn  15229  fiinopn  15230  iscld  15329  iuncld  15341  tgrest  15395  iscn  15423  cnpval  15424  iscnp  15425  tgcn  15434  ssidcn  15436  lmbrf  15441  cnpnei  15445  cnima  15446  cnconst2  15459  cnrest2  15462  cnptopresti  15464  cnptoprest  15465  lmres  15474  lmtopcnp  15476  txbasval  15493  tx1cn  15495  tx2cn  15496  txcnp  15497  txcnmpt  15499  txdis1cn  15504  txlm  15505  cnmpt11  15509  cnmpt12  15513  cnmpt21  15517  cnmpt22  15520  ishmeo  15530  hmeoopn  15537  hmeocld  15538  qtopbasss  15747  fsumcncntop  15793  expcn  15795  expcncf  15835  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemdisj  15866  ivthinclemloc  15867  ivthinc  15869  ivthdec  15870  limccl  15885  ellimc3apf  15886  cnmptlimc  15900  limccoap  15904  dvmptfsum  15951  plycolemc  15984  plycj  15987  2irrexpq  16212  2irrexpqap  16214  zprmlogbap  16218  pellexlem1  16229  efnnfsumcl  16239  efchtqdvds  16265  fsumdvdsmul  16285  ppiqub  16293  perfect  16301  prmefexple  16308  bposlem1  16311  lgsval  16328  lgsval2lem  16334  lgsdir2lem4  16355  lgsdir2  16357  m1lgs  16409  2lgs  16428  mul2sq  16440  2sqlem6  16444  wlkcprim  16796  isclwwlk  16840  clwwlk1loop  16845  clwwlkccatlem  16846  clwwlkn1  16864  loopclwwlkn1b  16865  clwwlkn1loopb  16866  clwwlkn2  16867  clwwlkext2edg  16868  umgr2cwwk2dif  16870  s2elclwwlknon2  16882  clwwlknonex2lem2  16884  clwwlknonex2  16885  eupth2lem2dc  16905  eulerpathprum  16926  bdinex1g  17132  bj-intexr  17139  bj-prexg  17142  bj-uniex  17148  bj-uniexg  17149  bdunexb  17151  bj-indsuc  17159  wexmiddiffilem  17248  wexmiddifxy  17251  exmidsbthrlem  17273  qdencn  17278  repiecef  17283  iswomni0  17308