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  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  7452  isnumi  7528  cc2lem  7633  cc3  7635  addnidpig  7704  indpi  7710  dfplpq2  7722  addclnq  7743  mulclnq  7744  nnnq0lem1  7814  addclnq0  7819  mulclnq0  7820  nqpnq0nq  7821  distrnq0  7827  prloc  7859  prarloclemlo  7862  prarloclem3  7865  prarloclem5  7868  genpml  7885  genpmu  7886  addnqprl  7897  addnqpru  7898  mulnqprl  7936  mulnqpru  7937  ltexprlemell  7966  ltexprlemelu  7967  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemrl  7978  ltexprlemru  7980  ltexpri  7981  recexprlemm  7992  recexprlemdisj  7998  recexprlemloc  7999  recexprlem1ssl  8001  recexprlem1ssu  8002  recexpr  8006  addclsr  8121  mulclsr  8122  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  suplocsr  8177  pitonn  8216  peano2nnnn  8221  axaddrcl  8233  axmulrcl  8235  peano5nnnn  8260  axpre-suploclemres  8269  negreb  8593  negf1o  8711  eqord1  8813  eqord2  8814  cju  9294  indfval  9302  peano2nn  9319  nn1m1nn  9325  nnaddcl  9327  nnmulcl  9328  nnsub  9346  nndivtr  9349  un0addcl  9601  un0mulcl  9602  elnnnn0  9611  fcdmnn0fsuppg  9623  elz  9651  nnnegz  9652  znegclb  9682  zaddcllempos  9686  zaddcllemneg  9688  zaddcl  9689  nzadd  9702  zmulcl  9703  elz2  9721  zneo  9752  nneoor  9753  zeo  9756  peano5uzti  9759  zindd  9769  uzp1  9966  uzaddcl  9996  supinfneg  10005  infsupneg  10006  supminfex  10007  ublbneg  10023  eqreznegel  10024  negm  10025  qmulz  10033  qnegcl  10046  irradd  10056  irrmul  10058  fzsplit3  10469  fzspl  10487  fzrev2  10503  infssuzex  10677  infssuzcldc  10679  zsupssdc  10684  negqmod0  10783  frec2uzuzd  10854  frecuzrdgrrn  10860  frec2uzrdg  10861  frecuzrdgrcl  10862  frecuzrdgsuc  10866  frecuzrdgrclt  10867  frecuzrdgg  10868  frecuzrdgsuctlem  10875  xnn0nnen  10889  iseqovex  10910  seq3val  10912  seqvalcd  10913  seq3-1  10914  seqf  10916  seq3p1  10917  seqovcd  10919  seqp1cd  10922  seq3clss  10923  monoord  10937  monoord2  10938  ser3mono  10939  seq3split  10940  seqsplitg  10941  seq3caopr3  10943  seq3caopr2  10945  seqcaopr2g  10946  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  iseqf1olemfvp  10962  seq3f1olemqsumkj  10963  seq3f1olemqsum  10965  seq3f1oleml  10968  seq3f1o  10969  seqf1og  10973  seq3homo  10979  seq3z  10980  seqhomog  10982  seqfeq4g  10983  seq3distr  10984  ser3ge0  10988  expp1  10998  expcllem  11002  expcl2lemap  11003  m1expcl2  11013  facnn  11181  fac0  11182  fac1  11183  faccl  11189  facdiv  11192  facndiv  11193  bccmpl  11208  bcn2  11218  bccl  11221  fihasheqf1oi  11242  hashf1lem2  11302  seq3coll  11310  ccatalpha  11397  reuccatpfxs1lem  11534  reuccatpfxs1  11535  shftlem  11597  shftf  11611  seq3shft  11619  cjval  11626  cjth  11627  remim  11641  uzin2  11769  caubnd2  11900  negfi  12011  xrmaxltsup  12043  clim  12066  clim2  12068  climshftlemg  12087  climcn1  12093  climcn2  12094  iserex  12124  climub  12129  climserle  12130  climcau  12132  serf0  12137  sumfct  12159  sumrbdclem  12163  fsum3cvg  12164  summodclem3  12166  summodclem2a  12167  zsumdc  12170  fsumgcl  12172  fsum3  12173  fsumf1o  12176  isumss  12177  isumss2  12179  fsum3cvg2  12180  fsum3ser  12183  fsumcl2lem  12184  fsumsplitf  12194  sumpr  12199  sumtp  12200  fsumm1  12202  fsum1p  12204  isummulc2  12212  fsum2dlemstep  12220  fisumcom2  12224  fsumshftm  12231  fisum0diag2  12233  fsummulc2  12234  fsumge1  12247  fsum00  12248  fsumabs  12251  telfsumo  12252  telfsumo2  12253  fsumparts  12256  fsumrelem  12257  fsumiun  12263  binomlem  12269  isumshft  12276  isum1p  12278  isumrpcl  12280  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemseq  12312  cvgratnnlemabsle  12313  cvgratnnlemfm  12315  cvgratnnlemrate  12316  cvgratnn  12317  cvgratz  12318  mertenslem2  12322  mertensabs  12323  clim2prod  12325  prodfap0  12331  prodfrecap  12332  prodfdivap  12333  prodrbdclem  12357  fproddccvg  12358  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  prodfct  12373  fprodf1o  12374  prodssdc  12375  fprodssdc  12376  fprodmul  12377  fprodm1  12384  fprod1p  12385  fprodm1s  12387  fprodp1s  12388  fprodcl2lem  12391  fprodabs  12402  fprod2dlemstep  12408  fprodcnv  12411  fprodcom2fi  12412  fprodrec  12415  fproddivapf  12417  fprodsplitf  12418  fprodsplit1f  12420  fprodle  12426  zeo3  12654  mulsucdiv2z  12671  zob  12677  nn0o1gt2  12691  nno  12692  nn0o  12693  uzwodc  12833  qnumdencl  12986  pcqcl  13108  pcxnn0cl  13112  pcxcl  13113  pcgcd1  13130  dvdsprmpweqle  13139  pcmpt  13145  pcmpt2  13146  pcmptdvds  13147  infpnlem2  13162  1arith  13169  elgz  13173  mul4sq  13196  4sqlem13m  13205  4sqlem17  13209  4sqlem18  13210  4sqlem19  13211  ballotfilemsdom  13307  ballotfilemrv  13315  ballotfilemrv1  13316  ballotfilemrv2  13317  ballotfilem1ri  13330  znnen  13341  ennnfonelemj0  13344  ennnfonelemg  13346  ennnfonelemom  13351  ctinfom  13371  ctiunctlemu1st  13377  ctiunctlemu2nd  13378  ctiunctlemudc  13380  ctiunctlemfo  13382  ssnnctlemct  13389  infpn2  13399  isstruct2im  13414  isstruct2r  13415  imasaddfnlemg  13688  ercpbl  13705  xpsfrnel2  13720  mgmsscl  13734  mgm1  13743  sgrppropd  13781  mndpropd  13806  issubm  13832  0subm  13844  insubm  13845  mhmima  13851  mulgsubcl  13992  issubg  14029  subgex  14032  issubg2m  14045  issubg4m  14049  0subg  14055  isnsg  14058  isnsg2  14059  nsgbi  14060  isnsg3  14063  elnmz  14064  nmzbi  14065  nmzsubg  14066  nmznsg  14069  releqgg  14076  eqgex  14077  eqgval  14079  eqgid  14082  ghmrn  14113  ghmnsgima  14124  eqgabl  14218  ablnsg  14222  gzsummhm2  14230  gsumvalfi  14236  gsumclfi  14243  gsummptfidmadd  14245  gsumsubmclfi  14247  gsummhm2fi  14249  isrng  14317  issrg  14353  srgfcl  14361  isring  14388  iscrng  14391  dvdsrd  14485  unitsubm  14510  isrim0  14552  issubrng  14591  subrngringnsg  14597  issubrng2  14602  opprsubrngg  14603  issubrg  14613  subrgsubm  14626  subrgugrp  14632  issubrg2  14633  issubrg3  14639  subrgpropd  14645  aprval  14675  aprunit  14676  aprsym  14680  opprdrng  14704  islmod  14711  lmodlema  14712  islmodd  14713  lmodprop2d  14769  rmodislmodlem  14771  rmodislmod  14772  lsssetm  14777  islssmd  14780  lssclg  14785  lsslss  14802  lsspropdg  14852  islidlm  14900  rnglidlmcl  14901  isridlrng  14903  rnglidlmmgm  14917  isridl  14925  gsumfsum  15007  psrbag  15137  psr1clfi  15170  uniopn  15193  inopn  15195  fiinopn  15196  iscld  15295  iuncld  15307  tgrest  15361  iscn  15389  cnpval  15390  iscnp  15391  tgcn  15400  ssidcn  15402  lmbrf  15407  cnpnei  15411  cnima  15412  cnconst2  15425  cnrest2  15428  cnptopresti  15430  cnptoprest  15431  lmres  15440  lmtopcnp  15442  txbasval  15459  tx1cn  15461  tx2cn  15462  txcnp  15463  txcnmpt  15465  txdis1cn  15470  txlm  15471  cnmpt11  15475  cnmpt12  15479  cnmpt21  15483  cnmpt22  15486  ishmeo  15496  hmeoopn  15503  hmeocld  15504  qtopbasss  15713  fsumcncntop  15759  expcn  15761  expcncf  15801  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemdisj  15832  ivthinclemloc  15833  ivthinc  15835  ivthdec  15836  limccl  15851  ellimc3apf  15852  cnmptlimc  15866  limccoap  15870  dvmptfsum  15917  plycolemc  15950  plycj  15953  2irrexpq  16173  2irrexpqap  16175  zprmlogbap  16179  pellexlem1  16190  efnnfsumcl  16200  efchtqdvds  16226  fsumdvdsmul  16246  ppiqub  16254  perfect  16262  prmefexple  16269  bposlem1  16272  lgsval  16289  lgsval2lem  16295  lgsdir2lem4  16316  lgsdir2  16318  m1lgs  16370  2lgs  16389  mul2sq  16401  2sqlem6  16405  wlkcprim  16757  isclwwlk  16801  clwwlk1loop  16806  clwwlkccatlem  16807  clwwlkn1  16825  loopclwwlkn1b  16826  clwwlkn1loopb  16827  clwwlkn2  16828  clwwlkext2edg  16829  umgr2cwwk2dif  16831  s2elclwwlknon2  16843  clwwlknonex2lem2  16845  clwwlknonex2  16846  eupth2lem2dc  16866  eulerpathprum  16887  bdinex1g  17093  bj-intexr  17100  bj-prexg  17103  bj-uniex  17109  bj-uniexg  17110  bdunexb  17112  bj-indsuc  17120  wexmiddiffilem  17209  wexmiddifxy  17212  exmidsbthrlem  17233  qdencn  17238  repiecef  17243  iswomni0  17268