Theorem eleq1d 2246

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12d  2248  eqeltrd  2254  eqneltrd  2273  eqneltrrd  2274  rspcimdv  2843  rspcimedv  2844  reuind  2943  sbcel2g  3079  sbccsb2g  3088  breq1  4007  breq2  4008  inex1g  4140  intexr  4151  pwexg  4181  prexg  4212  opelopabsb  4261  pofun  4313  seex  4336  uniex  4438  uniexg  4440  unexb  4443  abnexg  4447  reusv3  4461  rabxfrd  4470  onun2  4490  onsucelsucexmid  4530  ordsucunielexmid  4531  dcextest  4581  tfisi  4587  peano2  4595  seinxp  4698  opabid2  4759  opeliunxp2  4768  elrn2g  4818  opeldm  4831  opeldmg  4833  elreldm  4854  elrn2  4870  opelresg  4915  elsnres  4945  iss  4954  elimasng  4997  issref  5012  rnxpid  5064  unielrel  5157  dffun5r  5229  funopg  5251  brprcneu  5509  tz6.12f  5545  fvelrnb  5564  ssimaex  5578  dmfco  5585  fvmpt3  5596  mptfvex  5602  fvmptf  5609  respreima  5645  fvelrn  5648  ffnfvf  5676  ffvresb  5680  fmptco  5683  fmptcof  5684  fsn  5689  fressnfv  5704  fnex  5739  funfvima  5749  funfvima3  5751  f1mpt  5772  fliftfuns  5799  isoselem  5821  ovrspc2v  5901  ffnov  5979  fovcl  5980  ovmpos  5998  ov2gf  5999  ovg  6013  funimassov  6024  caovclg  6027  elovmpo  6072  off  6095  fnexALT  6112  focdmex  6116  f1stres  6160  f2ndres  6161  xp1st  6166  xp2nd  6167  elxp6  6170  oprssdmm  6172  unielxp  6175  fmpox  6201  mpofvex  6204  opeliunxp2f  6239  dftpos4  6264  smoel  6301  tfrlem3-2d  6313  tfrlem8  6319  tfrlem9  6320  tfrlemibxssdm  6328  tfrlemi1  6333  tfrexlem  6335  tfr1onlemsucfn  6341  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfr1onlemaccex  6349  tfr1onlemres  6350  tfri1dALT  6352  tfrcllemsucfn  6354  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemaccex  6362  tfrcllemres  6363  tfrcl  6365  rdgtfr  6375  rdgon  6387  frecabex  6399  frecabcl  6400  frecfcllem  6405  frecsuclem  6407  nnacl  6481  nnmcl  6482  nnmordi  6517  nnaordex  6529  nnm00  6531  erexb  6560  qliftfuns  6619  ixpsnval  6701  elixp2  6702  resixp  6733  mptelixpg  6734  elixpsn  6735  fundmen  6806  fopwdom  6836  xpf1o  6844  dif1en  6879  diffitest  6887  diffifi  6894  inffiexmid  6906  unfiexmid  6917  unfidisj  6921  fiintim  6928  xpfi  6929  ssfirab  6933  fnfi  6936  iunfidisj  6945  snexxph  6949  fidcenumlemr  6954  elfi2  6971  ctssdccl  7110  isnumi  7181  cc2lem  7265  cc3  7267  addnidpig  7335  indpi  7341  dfplpq2  7353  addclnq  7374  mulclnq  7375  nnnq0lem1  7445  addclnq0  7450  mulclnq0  7451  nqpnq0nq  7452  distrnq0  7458  prloc  7490  prarloclemlo  7493  prarloclem3  7496  prarloclem5  7499  genpml  7516  genpmu  7517  addnqprl  7528  addnqpru  7529  mulnqprl  7567  mulnqpru  7568  ltexprlemell  7597  ltexprlemelu  7598  ltexprlemdisj  7605  ltexprlemloc  7606  ltexprlemrl  7609  ltexprlemru  7611  ltexpri  7612  recexprlemm  7623  recexprlemdisj  7629  recexprlemloc  7630  recexprlem1ssl  7632  recexprlem1ssu  7633  recexpr  7637  addclsr  7752  mulclsr  7753  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  suplocsr  7808  pitonn  7847  peano2nnnn  7852  axaddrcl  7864  axmulrcl  7866  peano5nnnn  7891  axpre-suploclemres  7900  negreb  8222  negf1o  8339  eqord1  8440  eqord2  8441  cju  8918  peano2nn  8931  nn1m1nn  8937  nnaddcl  8939  nnmulcl  8940  nnsub  8958  nndivtr  8961  un0addcl  9209  un0mulcl  9210  elnnnn0  9219  elz  9255  nnnegz  9256  znegclb  9286  zaddcllempos  9290  zaddcllemneg  9292  zaddcl  9293  nzadd  9305  zmulcl  9306  elz2  9324  zneo  9354  nneoor  9355  zeo  9358  peano5uzti  9361  zindd  9371  uzp1  9561  uzaddcl  9586  supinfneg  9595  infsupneg  9596  supminfex  9597  ublbneg  9613  eqreznegel  9614  negm  9615  qmulz  9623  qnegcl  9636  irradd  9646  irrmul  9647  fzrev2  10085  negqmod0  10331  frec2uzuzd  10402  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdgrcl  10410  frecuzrdgsuc  10414  frecuzrdgrclt  10415  frecuzrdgg  10416  frecuzrdgsuctlem  10423  iseqovex  10456  seq3val  10458  seqvalcd  10459  seq3-1  10460  seqf  10461  seq3p1  10462  seqovcd  10463  seqp1cd  10466  seq3clss  10467  monoord  10476  monoord2  10477  ser3mono  10478  seq3split  10479  seq3caopr3  10481  seq3caopr2  10482  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  iseqf1olemfvp  10497  seq3f1olemqsumkj  10498  seq3f1olemqsum  10500  seq3f1oleml  10503  seq3f1o  10504  seq3homo  10510  seq3z  10511  seq3distr  10513  ser3ge0  10517  expp1  10527  expcllem  10531  expcl2lemap  10532  m1expcl2  10542  facnn  10707  fac0  10708  fac1  10709  faccl  10715  facdiv  10718  facndiv  10719  bccmpl  10734  bcn2  10744  bccl  10747  fihasheqf1oi  10767  seq3coll  10822  shftlem  10825  shftf  10839  seq3shft  10847  cjval  10854  cjth  10855  remim  10869  uzin2  10996  caubnd2  11126  negfi  11236  xrmaxltsup  11266  clim  11289  clim2  11291  climshftlemg  11310  climcn1  11316  climcn2  11317  iserex  11347  climub  11352  climserle  11353  climcau  11355  serf0  11360  sumfct  11382  sumrbdclem  11385  fsum3cvg  11386  summodclem3  11388  summodclem2a  11389  zsumdc  11392  fsumgcl  11394  fsum3  11395  fsumf1o  11398  isumss  11399  isumss2  11401  fsum3cvg2  11402  fsum3ser  11405  fsumcl2lem  11406  fsumsplitf  11416  sumpr  11421  sumtp  11422  fsumm1  11424  fsum1p  11426  isummulc2  11434  fsum2dlemstep  11442  fisumcom2  11446  fsumshftm  11453  fisum0diag2  11455  fsummulc2  11456  fsumge1  11469  fsum00  11470  fsumabs  11473  telfsumo  11474  telfsumo2  11475  fsumparts  11478  fsumrelem  11479  fsumiun  11485  binomlem  11491  isumshft  11498  isum1p  11500  isumrpcl  11502  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratnnlemseq  11534  cvgratnnlemabsle  11535  cvgratnnlemfm  11537  cvgratnnlemrate  11538  cvgratnn  11539  cvgratz  11540  mertenslem2  11544  mertensabs  11545  clim2prod  11547  prodfap0  11553  prodfrecap  11554  prodfdivap  11555  prodrbdclem  11579  fproddccvg  11580  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  prodfct  11595  fprodf1o  11596  prodssdc  11597  fprodssdc  11598  fprodmul  11599  fprodm1  11606  fprod1p  11607  fprodm1s  11609  fprodp1s  11610  fprodcl2lem  11613  fprodabs  11624  fprod2dlemstep  11630  fprodcnv  11633  fprodcom2fi  11634  fprodrec  11637  fproddivapf  11639  fprodsplitf  11640  fprodsplit1f  11642  fprodle  11648  zeo3  11873  mulsucdiv2z  11890  zob  11896  nn0o1gt2  11910  nno  11911  nn0o  11912  infssuzex  11950  infssuzcldc  11952  zsupssdc  11955  uzwodc  12038  qnumdencl  12187  pcqcl  12306  pcxnn0cl  12310  pcxcl  12311  pcgcd1  12327  dvdsprmpweqle  12336  pcmpt  12341  pcmpt2  12342  pcmptdvds  12343  infpnlem2  12358  1arith  12365  elgz  12369  mul4sq  12392  znnen  12399  ennnfonelemj0  12402  ennnfonelemg  12404  ennnfonelemom  12409  ctinfom  12429  ctiunctlemu1st  12435  ctiunctlemu2nd  12436  ctiunctlemudc  12438  ctiunctlemfo  12440  ssnnctlemct  12447  infpn2  12457  isstruct2im  12472  isstruct2r  12473  imasaddfnlemg  12735  ercpbl  12750  xpsfrnel2  12765  mgmsscl  12780  mgm1  12789  mndpropd  12841  issubm  12863  0subm  12871  insubm  12872  mhmima  12875  mulgsubcl  12997  issubg  13033  subgex  13036  issubg2m  13049  issubg4m  13053  0subg  13059  isnsg  13062  isnsg2  13063  nsgbi  13064  isnsg3  13067  elnmz  13068  nmzbi  13069  nmzsubg  13070  nmznsg  13073  releqgg  13080  eqgval  13082  eqgid  13085  issrg  13148  srgfcl  13156  isring  13183  iscrng  13186  dvdsrd  13263  unitsubm  13288  issubrg  13342  subrgsubm  13355  subrgugrp  13361  issubrg2  13362  issubrg3  13368  subrgpropd  13369  aprval  13372  aprsym  13374  islmod  13381  lmodlema  13382  islmodd  13383  lmodprop2d  13438  rmodislmodlem  13440  rmodislmod  13441  uniopn  13504  inopn  13506  fiinopn  13507  iscld  13606  iuncld  13618  tgrest  13672  iscn  13700  cnpval  13701  iscnp  13702  tgcn  13711  ssidcn  13713  lmbrf  13718  cnpnei  13722  cnima  13723  cnconst2  13736  cnrest2  13739  cnptopresti  13741  cnptoprest  13742  lmres  13751  lmtopcnp  13753  txbasval  13770  tx1cn  13772  tx2cn  13773  txcnp  13774  txcnmpt  13776  txdis1cn  13781  txlm  13782  cnmpt11  13786  cnmpt12  13790  cnmpt21  13794  cnmpt22  13797  ishmeo  13807  hmeoopn  13814  hmeocld  13815  qtopbasss  14024  fsumcncntop  14059  expcncf  14095  ivthinclemlopn  14117  ivthinclemlr  14118  ivthinclemuopn  14119  ivthinclemur  14120  ivthinclemdisj  14121  ivthinclemloc  14122  ivthinc  14124  ivthdec  14125  limccl  14131  ellimc3apf  14132  cnmptlimc  14146  limccoap  14150  2irrexpq  14397  2irrexpqap  14399  lgsval  14408  lgsval2lem  14414  lgsdir2lem4  14435  lgsdir2  14437  m1lgs  14455  mul2sq  14466  2sqlem6  14470  bdinex1g  14656  bj-intexr  14663  bj-prexg  14666  bj-uniex  14672  bj-uniexg  14673  bdunexb  14675  bj-indsuc  14683  exmidsbthrlem  14773  qdencn  14778  iswomni0  14802