Theorem eleq1d 2307

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 2301	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ 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  6514  dftpos4  6539  smoel  6576  tfrlem3-2d  6588  tfrlem8  6594  tfrlem9  6595  tfrlemibxssdm  6603  tfrlemi1  6608  tfrexlem  6610  tfr1onlemsucfn  6616  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemaccex  6624  tfr1onlemres  6625  tfri1dALT  6627  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemaccex  6637  tfrcllemres  6638  tfrcl  6640  rdgtfr  6650  rdgon  6662  frecabex  6674  frecabcl  6675  frecfcllem  6680  frecsuclem  6682  nnacl  6758  nnmcl  6759  nnmordi  6794  nnaordex  6806  nnm00  6808  erexb  6837  qliftfuns  6898  ixpsnval  6989  elixp2  6990  resixp  7021  mptelixpg  7022  elixpsn  7023  fundmen  7100  fopwdom  7142  xpf1o  7150  dif1en  7189  diffitest  7197  diffifi  7204  inffiexmid  7219  unfiexmid  7231  unfidisj  7235  prfidceq  7241  fiintim  7244  xpfi  7245  ssfirab  7250  fnfi  7256  iunfidisj  7266  mapfi  7267  relresfin  7270  snexxph  7274  fidcenumlemr  7279  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  elz  9655  nnnegz  9656  znegclb  9686  zaddcllempos  9690  zaddcllemneg  9692  zaddcl  9693  nzadd  9706  zmulcl  9707  elz2  9725  fcdmnn0fsuppfi  9743  zneo  9757  nneoor  9758  zeo  9761  peano5uzti  9764  zindd  9774  uzp1  9971  uzaddcl  10001  supinfneg  10010  infsupneg  10011  supminfex  10012  ublbneg  10028  eqreznegel  10029  negm  10030  qmulz  10038  qnegcl  10051  irradd  10061  irrmul  10063  fzsplit3  10474  fzspl  10492  fzrev2  10508  infssuzex  10682  infssuzcldc  10684  zsupssdc  10689  negqmod0  10788  frec2uzuzd  10859  frecuzrdgrrn  10865  frec2uzrdg  10866  frecuzrdgrcl  10867  frecuzrdgsuc  10871  frecuzrdgrclt  10872  frecuzrdgg  10873  frecuzrdgsuctlem  10880  xnn0nnen  10894  iseqovex  10915  seq3val  10917  seqvalcd  10918  seq3-1  10919  seqf  10921  seq3p1  10922  seqovcd  10924  seqp1cd  10927  seq3clss  10928  monoord  10942  monoord2  10943  ser3mono  10944  seq3split  10945  seqsplitg  10946  seq3caopr3  10948  seq3caopr2  10950  seqcaopr2g  10951  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  iseqf1olemfvp  10967  seq3f1olemqsumkj  10968  seq3f1olemqsum  10970  seq3f1oleml  10973  seq3f1o  10974  seqf1og  10978  seq3homo  10984  seq3z  10985  seqhomog  10987  seqfeq4g  10988  seq3distr  10989  ser3ge0  10993  expp1  11003  expcllem  11007  expcl2lemap  11008  m1expcl2  11018  facnn  11186  fac0  11187  fac1  11188  faccl  11194  facdiv  11197  facndiv  11198  bccmpl  11213  bcn2  11223  bccl  11226  fihasheqf1oi  11247  hashf1lem2  11307  seq3coll  11315  ccatalpha  11402  reuccatpfxs1lem  11539  reuccatpfxs1  11540  shftlem  11602  shftf  11616  seq3shft  11624  cjval  11631  cjth  11632  remim  11646  uzin2  11774  caubnd2  11905  negfi  12016  xrmaxltsup  12048  clim  12071  clim2  12073  climshftlemg  12092  climcn1  12098  climcn2  12099  iserex  12129  climub  12134  climserle  12135  climcau  12137  serf0  12142  sumfct  12164  sumrbdclem  12168  fsum3cvg  12169  summodclem3  12171  summodclem2a  12172  zsumdc  12175  fsumgcl  12177  fsum3  12178  fsumf1o  12181  isumss  12182  isumss2  12184  fsum3cvg2  12185  fsum3ser  12188  fsumcl2lem  12189  fsumsplitf  12199  sumpr  12204  sumtp  12205  fsumm1  12207  fsum1p  12209  isummulc2  12217  fsum2dlemstep  12225  fisumcom2  12229  fsumshftm  12236  fisum0diag2  12238  fsummulc2  12239  fsumge1  12252  fsum00  12253  fsumabs  12256  telfsumo  12257  telfsumo2  12258  fsumparts  12261  fsumrelem  12262  fsumiun  12268  binomlem  12274  isumshft  12281  isum1p  12283  isumrpcl  12285  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratnnlemseq  12317  cvgratnnlemabsle  12318  cvgratnnlemfm  12320  cvgratnnlemrate  12321  cvgratnn  12322  cvgratz  12323  mertenslem2  12327  mertensabs  12328  clim2prod  12330  prodfap0  12336  prodfrecap  12337  prodfdivap  12338  prodrbdclem  12362  fproddccvg  12363  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  prodfct  12378  fprodf1o  12379  prodssdc  12380  fprodssdc  12381  fprodmul  12382  fprodm1  12389  fprod1p  12390  fprodm1s  12392  fprodp1s  12393  fprodcl2lem  12396  fprodabs  12407  fprod2dlemstep  12413  fprodcnv  12416  fprodcom2fi  12417  fprodrec  12420  fproddivapf  12422  fprodsplitf  12423  fprodsplit1f  12425  fprodle  12431  zeo3  12659  mulsucdiv2z  12676  zob  12682  nn0o1gt2  12696  nno  12697  nn0o  12698  uzwodc  12838  qnumdencl  12991  pcqcl  13113  pcxnn0cl  13117  pcxcl  13118  pcgcd1  13135  dvdsprmpweqle  13144  pcmpt  13150  pcmpt2  13151  pcmptdvds  13152  infpnlem2  13167  1arith  13174  elgz  13178  mul4sq  13201  4sqlem13m  13210  4sqlem17  13214  4sqlem18  13215  4sqlem19  13216  ballotfilemsdom  13312  ballotfilemrv  13320  ballotfilemrv1  13321  ballotfilemrv2  13322  ballotfilem1ri  13335  znnen  13346  ennnfonelemj0  13349  ennnfonelemg  13351  ennnfonelemom  13356  ctinfom  13376  ctiunctlemu1st  13382  ctiunctlemu2nd  13383  ctiunctlemudc  13385  ctiunctlemfo  13387  ssnnctlemct  13394  infpn2  13404  isstruct2im  13419  isstruct2r  13420  imasaddfnlemg  13693  ercpbl  13710  xpsfrnel2  13725  mgmsscl  13739  mgm1  13748  sgrppropd  13786  mndpropd  13811  issubm  13837  0subm  13849  insubm  13850  mhmima  13856  mulgsubcl  13997  issubg  14034  subgex  14037  issubg2m  14050  issubg4m  14054  0subg  14060  isnsg  14063  isnsg2  14064  nsgbi  14065  isnsg3  14068  elnmz  14069  nmzbi  14070  nmzsubg  14071  nmznsg  14074  releqgg  14081  eqgex  14082  eqgval  14084  eqgid  14087  ghmrn  14118  ghmnsgima  14129  eqgabl  14223  ablnsg  14227  gzsummhm2  14235  gsumvalfi  14241  gsumclfi  14248  gsummptfidmadd  14250  gsumsubmclfi  14252  gsummptfidmsplit  14253  gsummhm2fi  14264  idjusnfi  14269  gsum2dfilem2  14271  gsumcom2fi  14274  isrng  14339  issrg  14375  srgfcl  14383  isring  14410  iscrng  14413  dvdsrd  14509  unitsubm  14534  isrim0  14576  issubrng  14615  subrngringnsg  14621  issubrng2  14626  opprsubrngg  14627  issubrg  14637  subrgsubm  14650  subrgugrp  14656  issubrg2  14657  issubrg3  14663  subrgpropd  14669  aprval  14699  aprunit  14700  aprsym  14704  opprdrng  14728  islmod  14735  lmodlema  14736  islmodd  14737  lmodprop2d  14793  rmodislmodlem  14795  rmodislmod  14796  lsssetm  14801  islssmd  14804  lssclg  14809  lsslss  14826  lsspropdg  14876  islidlm  14924  rnglidlmcl  14925  isridlrng  14927  rnglidlmmgm  14941  isridl  14949  gsumfsum  15031  psrbag  15163  psr1clfi  15207  uniopn  15244  inopn  15246  fiinopn  15247  iscld  15346  iuncld  15358  tgrest  15412  iscn  15440  cnpval  15441  iscnp  15442  tgcn  15451  ssidcn  15453  lmbrf  15458  cnpnei  15462  cnima  15463  cnconst2  15476  cnrest2  15479  cnptopresti  15481  cnptoprest  15482  lmres  15491  lmtopcnp  15493  txbasval  15510  tx1cn  15512  tx2cn  15513  txcnp  15514  txcnmpt  15516  txdis1cn  15521  txlm  15522  cnmpt11  15526  cnmpt12  15530  cnmpt21  15534  cnmpt22  15537  ishmeo  15547  hmeoopn  15554  hmeocld  15555  qtopbasss  15764  fsumcncntop  15810  expcn  15812  expcncf  15852  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemdisj  15883  ivthinclemloc  15884  ivthinc  15886  ivthdec  15887  limccl  15902  ellimc3apf  15903  cnmptlimc  15917  limccoap  15921  dvmptfsum  15968  plycolemc  16001  plycj  16004  2irrexpq  16229  2irrexpqap  16231  zprmlogbap  16235  pellexlem1  16246  efnnfsumcl  16256  efchtqdvds  16282  fsumdvdsmul  16302  ppiqub  16310  perfect  16318  prmefexple  16325  bposlem1  16328  lgsval  16345  lgsval2lem  16351  lgsdir2lem4  16372  lgsdir2  16374  m1lgs  16426  2lgs  16445  mul2sq  16457  2sqlem6  16461  wlkcprim  16813  isclwwlk  16857  clwwlk1loop  16862  clwwlkccatlem  16863  clwwlkn1  16881  loopclwwlkn1b  16882  clwwlkn1loopb  16883  clwwlkn2  16884  clwwlkext2edg  16885  umgr2cwwk2dif  16887  s2elclwwlknon2  16899  clwwlknonex2lem2  16901  clwwlknonex2  16902  eupth2lem2dc  16922  eulerpathprum  16943  bdinex1g  17149  bj-intexr  17156  bj-prexg  17159  bj-uniex  17165  bj-uniexg  17166  bdunexb  17168  bj-indsuc  17176  wexmiddiffilem  17265  wexmiddifxy  17268  exmidsbthrlem  17290  qdencn  17295  repiecef  17300  iswomni0  17325