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  4133  breq2  4134  inex1g  4269  intexr  4286  pwexg  4317  prexg  4349  opelopabsb  4402  pofun  4457  seex  4480  uniex  4583  uniexg  4585  unexb  4588  abnexg  4592  reusv3  4606  rabxfrd  4615  onun2  4637  onsucelsucexmid  4677  ordsucunielexmid  4678  dcextest  4728  tfisi  4734  peano2  4742  seinxp  4846  opabid2  4911  opeliunxp2  4920  elrn2g  4970  opeldm  4984  opeldmg  4986  elreldm  5008  elrn2  5024  opelresg  5070  elsnres  5100  iss  5109  xpexcnvm  5142  elimasng  5155  issref  5170  rnxpid  5222  unielrel  5315  dffun5r  5389  funopg  5411  brprcneu  5688  tz6.12f  5724  fvelrnb  5750  ssimaex  5764  dmfco  5773  fvmpt3  5784  mptfvex  5791  fvmptf  5798  respreima  5836  fvelrn  5839  ffnfvf  5867  ffvresb  5871  fmptco  5874  fmptcof  5875  fsn  5880  fsn2g  5883  fressnfv  5902  fnex  5937  funfvima  5950  funfvima3  5952  f1mpt  5977  fliftfuns  6004  isoselem  6026  ovrspc2v  6111  ffnov  6192  fovcld  6193  ovmpos  6212  ov2gf  6213  ovg  6228  funimassov  6239  caovclg  6242  elovmpo  6288  off  6315  caofdig  6336  fnexALT  6340  focdmex  6344  f1stres  6393  f2ndres  6394  xp1st  6399  xp2nd  6400  elxp6  6403  oprssdmm  6405  unielxp  6408  fmpox  6436  mpofvex  6441  elmpom  6474  suppofss1dcl  6504  suppofss2dcl  6505  opeliunxp2f  6509  dftpos4  6534  smoel  6571  tfrlem3-2d  6583  tfrlem8  6589  tfrlem9  6590  tfrlemibxssdm  6598  tfrlemi1  6603  tfrexlem  6605  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  rdgtfr  6645  rdgon  6657  frecabex  6669  frecabcl  6670  frecfcllem  6675  frecsuclem  6677  nnacl  6753  nnmcl  6754  nnmordi  6789  nnaordex  6801  nnm00  6803  erexb  6832  qliftfuns  6893  ixpsnval  6983  elixp2  6984  resixp  7015  mptelixpg  7016  elixpsn  7017  fundmen  7094  fopwdom  7136  xpf1o  7144  dif1en  7183  diffitest  7191  diffifi  7198  inffiexmid  7213  unfiexmid  7225  unfidisj  7229  prfidceq  7235  fiintim  7238  xpfi  7239  ssfirab  7244  fnfi  7250  iunfidisj  7260  mapfi  7261  snexxph  7267  fidcenumlemr  7272  isfsupp  7289  ffsuppbi  7300  elfi2  7306  ctssdccl  7451  isnumi  7527  cc2lem  7632  cc3  7634  addnidpig  7703  indpi  7709  dfplpq2  7721  addclnq  7742  mulclnq  7743  nnnq0lem1  7813  addclnq0  7818  mulclnq0  7819  nqpnq0nq  7820  distrnq0  7826  prloc  7858  prarloclemlo  7861  prarloclem3  7864  prarloclem5  7867  genpml  7884  genpmu  7885  addnqprl  7896  addnqpru  7897  mulnqprl  7935  mulnqpru  7936  ltexprlemell  7965  ltexprlemelu  7966  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  ltexpri  7980  recexprlemm  7991  recexprlemdisj  7997  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  recexpr  8005  addclsr  8120  mulclsr  8121  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  suplocsr  8176  pitonn  8215  peano2nnnn  8220  axaddrcl  8232  axmulrcl  8234  peano5nnnn  8259  axpre-suploclemres  8268  negreb  8592  negf1o  8710  eqord1  8812  eqord2  8813  cju  9293  indfval  9301  peano2nn  9318  nn1m1nn  9324  nnaddcl  9326  nnmulcl  9327  nnsub  9345  nndivtr  9348  un0addcl  9600  un0mulcl  9601  elnnnn0  9610  fcdmnn0fsuppg  9622  elz  9650  nnnegz  9651  znegclb  9681  zaddcllempos  9685  zaddcllemneg  9687  zaddcl  9688  nzadd  9701  zmulcl  9702  elz2  9720  zneo  9751  nneoor  9752  zeo  9755  peano5uzti  9758  zindd  9768  uzp1  9965  uzaddcl  9995  supinfneg  10004  infsupneg  10005  supminfex  10006  ublbneg  10022  eqreznegel  10023  negm  10024  qmulz  10032  qnegcl  10045  irradd  10055  irrmul  10057  fzsplit3  10468  fzspl  10486  fzrev2  10502  infssuzex  10676  infssuzcldc  10678  zsupssdc  10683  negqmod0  10781  frec2uzuzd  10852  frecuzrdgrrn  10858  frec2uzrdg  10859  frecuzrdgrcl  10860  frecuzrdgsuc  10864  frecuzrdgrclt  10865  frecuzrdgg  10866  frecuzrdgsuctlem  10873  xnn0nnen  10887  iseqovex  10908  seq3val  10910  seqvalcd  10911  seq3-1  10912  seqf  10914  seq3p1  10915  seqovcd  10917  seqp1cd  10920  seq3clss  10921  monoord  10935  monoord2  10936  ser3mono  10937  seq3split  10938  seqsplitg  10939  seq3caopr3  10941  seq3caopr2  10943  seqcaopr2g  10944  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  iseqf1olemfvp  10960  seq3f1olemqsumkj  10961  seq3f1olemqsum  10963  seq3f1oleml  10966  seq3f1o  10967  seqf1og  10971  seq3homo  10977  seq3z  10978  seqhomog  10980  seqfeq4g  10981  seq3distr  10982  ser3ge0  10986  expp1  10996  expcllem  11000  expcl2lemap  11001  m1expcl2  11011  facnn  11179  fac0  11180  fac1  11181  faccl  11187  facdiv  11190  facndiv  11191  bccmpl  11206  bcn2  11216  bccl  11219  fihasheqf1oi  11240  hashf1lem2  11300  seq3coll  11308  ccatalpha  11395  reuccatpfxs1lem  11532  reuccatpfxs1  11533  shftlem  11595  shftf  11609  seq3shft  11617  cjval  11624  cjth  11625  remim  11639  uzin2  11767  caubnd2  11898  negfi  12009  xrmaxltsup  12040  clim  12063  clim2  12065  climshftlemg  12084  climcn1  12090  climcn2  12091  iserex  12121  climub  12126  climserle  12127  climcau  12129  serf0  12134  sumfct  12156  sumrbdclem  12160  fsum3cvg  12161  summodclem3  12163  summodclem2a  12164  zsumdc  12167  fsumgcl  12169  fsum3  12170  fsumf1o  12173  isumss  12174  isumss2  12176  fsum3cvg2  12177  fsum3ser  12180  fsumcl2lem  12181  fsumsplitf  12191  sumpr  12196  sumtp  12197  fsumm1  12199  fsum1p  12201  isummulc2  12209  fsum2dlemstep  12217  fisumcom2  12221  fsumshftm  12228  fisum0diag2  12230  fsummulc2  12231  fsumge1  12244  fsum00  12245  fsumabs  12248  telfsumo  12249  telfsumo2  12250  fsumparts  12253  fsumrelem  12254  fsumiun  12260  binomlem  12266  isumshft  12273  isum1p  12275  isumrpcl  12277  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratnnlemseq  12309  cvgratnnlemabsle  12310  cvgratnnlemfm  12312  cvgratnnlemrate  12313  cvgratnn  12314  cvgratz  12315  mertenslem2  12319  mertensabs  12320  clim2prod  12322  prodfap0  12328  prodfrecap  12329  prodfdivap  12330  prodrbdclem  12354  fproddccvg  12355  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  prodfct  12370  fprodf1o  12371  prodssdc  12372  fprodssdc  12373  fprodmul  12374  fprodm1  12381  fprod1p  12382  fprodm1s  12384  fprodp1s  12385  fprodcl2lem  12388  fprodabs  12399  fprod2dlemstep  12405  fprodcnv  12408  fprodcom2fi  12409  fprodrec  12412  fproddivapf  12414  fprodsplitf  12415  fprodsplit1f  12417  fprodle  12423  zeo3  12651  mulsucdiv2z  12668  zob  12674  nn0o1gt2  12688  nno  12689  nn0o  12690  uzwodc  12830  qnumdencl  12983  pcqcl  13105  pcxnn0cl  13109  pcxcl  13110  pcgcd1  13127  dvdsprmpweqle  13136  pcmpt  13142  pcmpt2  13143  pcmptdvds  13144  infpnlem2  13159  1arith  13166  elgz  13170  mul4sq  13193  4sqlem13m  13202  4sqlem17  13206  4sqlem18  13207  4sqlem19  13208  ballotfilemsdom  13304  ballotfilemrv  13312  ballotfilemrv1  13313  ballotfilemrv2  13314  ballotfilem1ri  13327  znnen  13338  ennnfonelemj0  13341  ennnfonelemg  13343  ennnfonelemom  13348  ctinfom  13368  ctiunctlemu1st  13374  ctiunctlemu2nd  13375  ctiunctlemudc  13377  ctiunctlemfo  13379  ssnnctlemct  13386  infpn2  13396  isstruct2im  13411  isstruct2r  13412  imasaddfnlemg  13684  ercpbl  13701  xpsfrnel2  13716  mgmsscl  13730  mgm1  13739  sgrppropd  13777  mndpropd  13802  issubm  13828  0subm  13840  insubm  13841  mhmima  13847  mulgsubcl  13988  issubg  14025  subgex  14028  issubg2m  14041  issubg4m  14045  0subg  14051  isnsg  14054  isnsg2  14055  nsgbi  14056  isnsg3  14059  elnmz  14060  nmzbi  14061  nmzsubg  14062  nmznsg  14065  releqgg  14072  eqgex  14073  eqgval  14075  eqgid  14078  ghmrn  14109  ghmnsgima  14120  eqgabl  14183  ablnsg  14187  gzsummhm2  14195  gsumvalfi  14201  gsumclfi  14208  gsummptfidmadd  14210  gsumsubmclfi  14212  gsummhm2fi  14214  isrng  14282  issrg  14318  srgfcl  14326  isring  14353  iscrng  14356  dvdsrd  14450  unitsubm  14475  isrim0  14517  issubrng  14556  subrngringnsg  14562  issubrng2  14567  opprsubrngg  14568  issubrg  14578  subrgsubm  14591  subrgugrp  14597  issubrg2  14598  issubrg3  14604  subrgpropd  14610  aprval  14640  aprunit  14641  aprsym  14645  opprdrng  14669  islmod  14676  lmodlema  14677  islmodd  14678  lmodprop2d  14734  rmodislmodlem  14736  rmodislmod  14737  lsssetm  14742  islssmd  14745  lssclg  14750  lsslss  14767  lsspropdg  14817  islidlm  14865  rnglidlmcl  14866  isridlrng  14868  rnglidlmmgm  14882  isridl  14890  gsumfsum  14972  psrbag  15102  psr1clfi  15128  uniopn  15151  inopn  15153  fiinopn  15154  iscld  15253  iuncld  15265  tgrest  15319  iscn  15347  cnpval  15348  iscnp  15349  tgcn  15358  ssidcn  15360  lmbrf  15365  cnpnei  15369  cnima  15370  cnconst2  15383  cnrest2  15386  cnptopresti  15388  cnptoprest  15389  lmres  15398  lmtopcnp  15400  txbasval  15417  tx1cn  15419  tx2cn  15420  txcnp  15421  txcnmpt  15423  txdis1cn  15428  txlm  15429  cnmpt11  15433  cnmpt12  15437  cnmpt21  15441  cnmpt22  15444  ishmeo  15454  hmeoopn  15461  hmeocld  15462  qtopbasss  15671  fsumcncntop  15717  expcn  15719  expcncf  15759  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemdisj  15790  ivthinclemloc  15791  ivthinc  15793  ivthdec  15794  limccl  15809  ellimc3apf  15810  cnmptlimc  15824  limccoap  15828  dvmptfsum  15875  plycolemc  15908  plycj  15911  2irrexpq  16131  2irrexpqap  16133  zprmlogbap  16137  pellexlem1  16148  fsumdvdsmul  16186  ppiqub  16194  perfect  16199  prmefexple  16206  bposlem1  16209  lgsval  16221  lgsval2lem  16227  lgsdir2lem4  16248  lgsdir2  16250  m1lgs  16302  2lgs  16321  mul2sq  16333  2sqlem6  16337  wlkcprim  16689  isclwwlk  16733  clwwlk1loop  16738  clwwlkccatlem  16739  clwwlkn1  16757  loopclwwlkn1b  16758  clwwlkn1loopb  16759  clwwlkn2  16760  clwwlkext2edg  16761  umgr2cwwk2dif  16763  s2elclwwlknon2  16775  clwwlknonex2lem2  16777  clwwlknonex2  16778  eupth2lem2dc  16798  eulerpathprum  16819  bdinex1g  17025  bj-intexr  17032  bj-prexg  17035  bj-uniex  17041  bj-uniexg  17042  bdunexb  17044  bj-indsuc  17052  wexmiddiffilem  17141  wexmiddifxy  17144  exmidsbthrlem  17165  qdencn  17170  repiecef  17175  iswomni0  17199