Theorem eleq1d 2303

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

Hypothesis

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eleq1d	⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Proof of Theorem eleq1d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eleq1 2297	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eleq12d  2305  eqeltrd  2311  eqneltrd  2330  eqneltrrd  2331  rspcimdv  2924  rspcimedv  2925  reuind  3024  sbcel2g  3161  sbccsb2g  3170  breq1  4114  breq2  4115  inex1g  4248  intexr  4264  pwexg  4295  prexg  4327  opelopabsb  4380  pofun  4435  seex  4458  uniex  4560  uniexg  4562  unexb  4565  abnexg  4569  reusv3  4583  rabxfrd  4592  onun2  4614  onsucelsucexmid  4654  ordsucunielexmid  4655  dcextest  4705  tfisi  4711  peano2  4719  seinxp  4823  opabid2  4888  opeliunxp2  4897  elrn2g  4947  opeldm  4961  opeldmg  4963  elreldm  4985  elrn2  5001  opelresg  5047  elsnres  5077  iss  5086  xpexcnvm  5119  elimasng  5132  issref  5147  rnxpid  5199  unielrel  5292  dffun5r  5366  funopg  5388  brprcneu  5665  tz6.12f  5701  fvelrnb  5726  ssimaex  5740  dmfco  5747  fvmpt3  5758  mptfvex  5765  fvmptf  5772  respreima  5807  fvelrn  5810  ffnfvf  5838  ffvresb  5842  fmptco  5845  fmptcof  5846  fsn  5851  fsn2g  5854  fressnfv  5873  fnex  5908  funfvima  5920  funfvima3  5922  f1mpt  5946  fliftfuns  5973  isoselem  5995  ovrspc2v  6078  ffnov  6159  fovcld  6160  ovmpos  6179  ov2gf  6180  ovg  6195  funimassov  6206  caovclg  6209  elovmpo  6255  off  6281  caofdig  6302  fnexALT  6306  focdmex  6310  f1stres  6355  f2ndres  6356  xp1st  6361  xp2nd  6362  elxp6  6365  oprssdmm  6367  unielxp  6370  fmpox  6398  mpofvex  6403  elmpom  6436  suppofss1dcl  6466  suppofss2dcl  6467  opeliunxp2f  6471  dftpos4  6496  smoel  6533  tfrlem3-2d  6545  tfrlem8  6551  tfrlem9  6552  tfrlemibxssdm  6560  tfrlemi1  6565  tfrexlem  6567  tfr1onlemsucfn  6573  tfr1onlemsucaccv  6574  tfr1onlembxssdm  6576  tfr1onlembfn  6577  tfr1onlemaccex  6581  tfr1onlemres  6582  tfri1dALT  6584  tfrcllemsucfn  6586  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllembfn  6590  tfrcllemaccex  6594  tfrcllemres  6595  tfrcl  6597  rdgtfr  6607  rdgon  6619  frecabex  6631  frecabcl  6632  frecfcllem  6637  frecsuclem  6639  nnacl  6715  nnmcl  6716  nnmordi  6751  nnaordex  6763  nnm00  6765  erexb  6794  qliftfuns  6855  ixpsnval  6938  elixp2  6939  resixp  6970  mptelixpg  6971  elixpsn  6972  fundmen  7049  fopwdom  7091  xpf1o  7099  dif1en  7138  diffitest  7146  diffifi  7153  inffiexmid  7168  unfiexmid  7180  unfidisj  7184  prfidceq  7190  fiintim  7193  xpfi  7194  ssfirab  7199  fnfi  7205  iunfidisj  7215  mapfi  7216  snexxph  7222  fidcenumlemr  7227  isfsupp  7244  ffsuppbi  7255  elfi2  7261  ctssdccl  7404  isnumi  7480  cc2lem  7582  cc3  7584  addnidpig  7653  indpi  7659  dfplpq2  7671  addclnq  7692  mulclnq  7693  nnnq0lem1  7763  addclnq0  7768  mulclnq0  7769  nqpnq0nq  7770  distrnq0  7776  prloc  7808  prarloclemlo  7811  prarloclem3  7814  prarloclem5  7817  genpml  7834  genpmu  7835  addnqprl  7846  addnqpru  7847  mulnqprl  7885  mulnqpru  7886  ltexprlemell  7915  ltexprlemelu  7916  ltexprlemdisj  7923  ltexprlemloc  7924  ltexprlemrl  7927  ltexprlemru  7929  ltexpri  7930  recexprlemm  7941  recexprlemdisj  7947  recexprlemloc  7948  recexprlem1ssl  7950  recexprlem1ssu  7951  recexpr  7955  addclsr  8070  mulclsr  8071  suplocsrlemb  8123  suplocsrlempr  8124  suplocsrlem  8125  suplocsr  8126  pitonn  8165  peano2nnnn  8170  axaddrcl  8182  axmulrcl  8184  peano5nnnn  8209  axpre-suploclemres  8218  negreb  8540  negf1o  8657  eqord1  8759  eqord2  8760  cju  9237  peano2nn  9251  nn1m1nn  9257  nnaddcl  9259  nnmulcl  9260  nnsub  9278  nndivtr  9281  un0addcl  9531  un0mulcl  9532  elnnnn0  9541  fcdmnn0fsuppg  9553  elz  9581  nnnegz  9582  znegclb  9612  zaddcllempos  9616  zaddcllemneg  9618  zaddcl  9619  nzadd  9632  zmulcl  9633  elz2  9651  zneo  9682  nneoor  9683  zeo  9686  peano5uzti  9689  zindd  9699  uzp1  9891  uzaddcl  9921  supinfneg  9930  infsupneg  9931  supminfex  9932  ublbneg  9948  eqreznegel  9949  negm  9950  qmulz  9958  qnegcl  9971  irradd  9981  irrmul  9982  fzspl  10407  fzrev2  10423  infssuzex  10597  infssuzcldc  10599  zsupssdc  10602  negqmod0  10697  frec2uzuzd  10768  frecuzrdgrrn  10774  frec2uzrdg  10775  frecuzrdgrcl  10776  frecuzrdgsuc  10780  frecuzrdgrclt  10781  frecuzrdgg  10782  frecuzrdgsuctlem  10789  xnn0nnen  10803  iseqovex  10824  seq3val  10826  seqvalcd  10827  seq3-1  10828  seqf  10830  seq3p1  10831  seqovcd  10833  seqp1cd  10836  seq3clss  10837  monoord  10851  monoord2  10852  ser3mono  10853  seq3split  10854  seqsplitg  10855  seq3caopr3  10857  seq3caopr2  10859  seqcaopr2g  10860  iseqf1olemjpcl  10874  iseqf1olemqpcl  10875  iseqf1olemfvp  10876  seq3f1olemqsumkj  10877  seq3f1olemqsum  10879  seq3f1oleml  10882  seq3f1o  10883  seqf1og  10887  seq3homo  10893  seq3z  10894  seqhomog  10896  seqfeq4g  10897  seq3distr  10898  ser3ge0  10902  expp1  10912  expcllem  10916  expcl2lemap  10917  m1expcl2  10927  facnn  11093  fac0  11094  fac1  11095  faccl  11101  facdiv  11104  facndiv  11105  bccmpl  11120  bcn2  11130  bccl  11133  fihasheqf1oi  11154  seq3coll  11218  ccatalpha  11305  reuccatpfxs1lem  11442  reuccatpfxs1  11443  shftlem  11505  shftf  11519  seq3shft  11527  cjval  11534  cjth  11535  remim  11549  uzin2  11676  caubnd2  11806  negfi  11917  xrmaxltsup  11947  clim  11970  clim2  11972  climshftlemg  11991  climcn1  11997  climcn2  11998  iserex  12028  climub  12033  climserle  12034  climcau  12036  serf0  12041  sumfct  12063  sumrbdclem  12067  fsum3cvg  12068  summodclem3  12070  summodclem2a  12071  zsumdc  12074  fsumgcl  12076  fsum3  12077  fsumf1o  12080  isumss  12081  isumss2  12083  fsum3cvg2  12084  fsum3ser  12087  fsumcl2lem  12088  fsumsplitf  12098  sumpr  12103  sumtp  12104  fsumm1  12106  fsum1p  12108  isummulc2  12116  fsum2dlemstep  12124  fisumcom2  12128  fsumshftm  12135  fisum0diag2  12137  fsummulc2  12138  fsumge1  12151  fsum00  12152  fsumabs  12155  telfsumo  12156  telfsumo2  12157  fsumparts  12160  fsumrelem  12161  fsumiun  12167  binomlem  12173  isumshft  12180  isum1p  12182  isumrpcl  12184  cvgratnnlemnexp  12214  cvgratnnlemmn  12215  cvgratnnlemseq  12216  cvgratnnlemabsle  12217  cvgratnnlemfm  12219  cvgratnnlemrate  12220  cvgratnn  12221  cvgratz  12222  mertenslem2  12226  mertensabs  12227  clim2prod  12229  prodfap0  12235  prodfrecap  12236  prodfdivap  12237  prodrbdclem  12261  fproddccvg  12262  prodmodclem3  12265  prodmodclem2a  12266  zproddc  12269  fprodseq  12273  prodfct  12277  fprodf1o  12278  prodssdc  12279  fprodssdc  12280  fprodmul  12281  fprodm1  12288  fprod1p  12289  fprodm1s  12291  fprodp1s  12292  fprodcl2lem  12295  fprodabs  12306  fprod2dlemstep  12312  fprodcnv  12315  fprodcom2fi  12316  fprodrec  12319  fproddivapf  12321  fprodsplitf  12322  fprodsplit1f  12324  fprodle  12330  zeo3  12558  mulsucdiv2z  12575  zob  12581  nn0o1gt2  12595  nno  12596  nn0o  12597  uzwodc  12737  qnumdencl  12888  pcqcl  13008  pcxnn0cl  13012  pcxcl  13013  pcgcd1  13030  dvdsprmpweqle  13039  pcmpt  13045  pcmpt2  13046  pcmptdvds  13047  infpnlem2  13062  1arith  13069  elgz  13073  mul4sq  13096  4sqlem13m  13105  4sqlem17  13109  4sqlem18  13110  4sqlem19  13111  znnen  13166  ennnfonelemj0  13169  ennnfonelemg  13171  ennnfonelemom  13176  ctinfom  13196  ctiunctlemu1st  13202  ctiunctlemu2nd  13203  ctiunctlemudc  13205  ctiunctlemfo  13207  ssnnctlemct  13214  infpn2  13224  isstruct2im  13239  isstruct2r  13240  imasaddfnlemg  13544  ercpbl  13561  xpsfrnel2  13576  mgmsscl  13591  mgm1  13600  sgrppropd  13643  mndpropd  13670  issubm  13702  0subm  13714  insubm  13715  mhmima  13721  mulgsubcl  13870  issubg  13907  subgex  13910  issubg2m  13923  issubg4m  13927  0subg  13933  isnsg  13936  isnsg2  13937  nsgbi  13938  isnsg3  13941  elnmz  13942  nmzbi  13943  nmzsubg  13944  nmznsg  13947  releqgg  13954  eqgex  13955  eqgval  13957  eqgid  13960  ghmrn  13991  ghmnsgima  14002  eqgabl  14064  ablnsg  14068  gsumfzmhm2  14078  isrng  14095  issrg  14126  srgfcl  14134  isring  14161  iscrng  14164  dvdsrd  14256  unitsubm  14281  isrim0  14323  issubrng  14361  subrngringnsg  14367  issubrng2  14372  opprsubrngg  14373  issubrg  14383  subrgsubm  14396  subrgugrp  14402  issubrg2  14403  issubrg3  14409  subrgpropd  14415  aprval  14445  aprsym  14447  islmod  14456  lmodlema  14457  islmodd  14458  lmodprop2d  14513  rmodislmodlem  14515  rmodislmod  14516  lsssetm  14521  islssmd  14524  lssclg  14529  lsslss  14546  lsspropdg  14596  islidlm  14644  rnglidlmcl  14645  isridlrng  14647  rnglidlmmgm  14661  isridl  14669  gsumfzfsumlemm  14752  psrbag  14834  psr1clfi  14860  uniopn  14883  inopn  14885  fiinopn  14886  iscld  14985  iuncld  14997  tgrest  15051  iscn  15079  cnpval  15080  iscnp  15081  tgcn  15090  ssidcn  15092  lmbrf  15097  cnpnei  15101  cnima  15102  cnconst2  15115  cnrest2  15118  cnptopresti  15120  cnptoprest  15121  lmres  15130  lmtopcnp  15132  txbasval  15149  tx1cn  15151  tx2cn  15152  txcnp  15153  txcnmpt  15155  txdis1cn  15160  txlm  15161  cnmpt11  15165  cnmpt12  15169  cnmpt21  15173  cnmpt22  15176  ishmeo  15186  hmeoopn  15193  hmeocld  15194  qtopbasss  15403  fsumcncntop  15449  expcn  15451  expcncf  15491  ivthinclemlopn  15518  ivthinclemlr  15519  ivthinclemuopn  15520  ivthinclemur  15521  ivthinclemdisj  15522  ivthinclemloc  15523  ivthinc  15525  ivthdec  15526  limccl  15541  ellimc3apf  15542  cnmptlimc  15556  limccoap  15560  dvmptfsum  15607  plycolemc  15640  plycj  15643  2irrexpq  15858  2irrexpqap  15860  pellexlem1  15862  fsumdvdsmul  15876  perfect  15886  lgsval  15894  lgsval2lem  15900  lgsdir2lem4  15921  lgsdir2  15923  m1lgs  15975  2lgs  15994  mul2sq  16006  2sqlem6  16010  wlkcprim  16362  isclwwlk  16406  clwwlk1loop  16411  clwwlkccatlem  16412  clwwlkn1  16430  loopclwwlkn1b  16431  clwwlkn1loopb  16432  clwwlkn2  16433  clwwlkext2edg  16434  umgr2cwwk2dif  16436  s2elclwwlknon2  16448  clwwlknonex2lem2  16450  clwwlknonex2  16451  eupth2lem2dc  16471  eulerpathprum  16492  bdinex1g  16688  bj-intexr  16695  bj-prexg  16698  bj-uniex  16704  bj-uniexg  16705  bdunexb  16707  bj-indsuc  16715  exmidsbthrlem  16819  qdencn  16824  repiecef  16829  iswomni0  16853  gfsumval  16879  gfsumcl  16887