Theorem eleq1d 2209

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332   ∈ wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  eleq12d  2211  eqeltrd  2217  eqneltrd  2236  eqneltrrd  2237  rspcimdv  2794  rspcimedv  2795  reuind  2893  sbcel2g  3028  sbccsb2g  3037  breq1  3940  breq2  3941  inex1g  4072  intexr  4083  pwexg  4112  prexg  4141  opelopabsb  4190  pofun  4242  seex  4265  uniex  4367  uniexg  4369  unexb  4371  abnexg  4375  reusv3  4389  rabxfrd  4398  onun2  4414  onsucelsucexmid  4453  ordsucunielexmid  4454  dcextest  4503  tfisi  4509  peano2  4517  seinxp  4618  opabid2  4678  opeliunxp2  4687  elrn2g  4737  opeldm  4750  opeldmg  4752  elreldm  4773  elrn2  4789  opelresg  4834  elsnres  4864  iss  4873  elimasng  4915  issref  4929  rnxpid  4981  unielrel  5074  dffun5r  5143  funopg  5165  brprcneu  5422  tz6.12f  5458  fvelrnb  5477  ssimaex  5490  dmfco  5497  fvmpt3  5508  mptfvex  5514  fvmptf  5521  respreima  5556  fvelrn  5559  ffnfvf  5587  ffvresb  5591  fmptco  5594  fmptcof  5595  fsn  5600  fressnfv  5615  fnex  5650  funfvima  5657  funfvima3  5659  f1mpt  5680  fliftfuns  5707  isoselem  5729  ffnov  5883  fovcl  5884  ovmpos  5902  ov2gf  5903  ovg  5917  funimassov  5928  caovclg  5931  elovmpo  5979  off  6002  fnexALT  6019  fornex  6021  f1stres  6065  f2ndres  6066  xp1st  6071  xp2nd  6072  elxp6  6075  oprssdmm  6077  unielxp  6080  fmpox  6106  mpofvex  6109  opeliunxp2f  6143  dftpos4  6168  smoel  6205  tfrlem3-2d  6217  tfrlem8  6223  tfrlem9  6224  tfrlemibxssdm  6232  tfrlemi1  6237  tfrexlem  6239  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemaccex  6253  tfr1onlemres  6254  tfri1dALT  6256  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemaccex  6266  tfrcllemres  6267  tfrcl  6269  rdgtfr  6279  rdgon  6291  frecabex  6303  frecabcl  6304  frecfcllem  6309  frecsuclem  6311  nnacl  6384  nnmcl  6385  nnmordi  6420  nnaordex  6431  nnm00  6433  erexb  6462  qliftfuns  6521  ixpsnval  6603  elixp2  6604  resixp  6635  mptelixpg  6636  elixpsn  6637  fundmen  6708  fopwdom  6738  xpf1o  6746  dif1en  6781  diffitest  6789  diffifi  6796  inffiexmid  6808  unfiexmid  6814  unfidisj  6818  fiintim  6825  xpfi  6826  ssfirab  6830  fnfi  6833  iunfidisj  6842  snexxph  6846  fidcenumlemr  6851  elfi2  6868  ctssdccl  7004  isnumi  7055  cc2lem  7098  cc3  7100  addnidpig  7168  indpi  7174  dfplpq2  7186  addclnq  7207  mulclnq  7208  nnnq0lem1  7278  addclnq0  7283  mulclnq0  7284  nqpnq0nq  7285  distrnq0  7291  prloc  7323  prarloclemlo  7326  prarloclem3  7329  prarloclem5  7332  genpml  7349  genpmu  7350  addnqprl  7361  addnqpru  7362  mulnqprl  7400  mulnqpru  7401  ltexprlemell  7430  ltexprlemelu  7431  ltexprlemdisj  7438  ltexprlemloc  7439  ltexprlemrl  7442  ltexprlemru  7444  ltexpri  7445  recexprlemm  7456  recexprlemdisj  7462  recexprlemloc  7463  recexprlem1ssl  7465  recexprlem1ssu  7466  recexpr  7470  addclsr  7585  mulclsr  7586  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  suplocsr  7641  pitonn  7680  peano2nnnn  7685  axaddrcl  7697  axmulrcl  7699  peano5nnnn  7724  axpre-suploclemres  7733  negreb  8051  negf1o  8168  eqord1  8269  eqord2  8270  cju  8743  peano2nn  8756  nn1m1nn  8762  nnaddcl  8764  nnmulcl  8765  nnsub  8783  nndivtr  8786  un0addcl  9034  un0mulcl  9035  elnnnn0  9044  elz  9080  nnnegz  9081  znegclb  9111  zaddcllempos  9115  zaddcllemneg  9117  zaddcl  9118  nzadd  9130  zmulcl  9131  elz2  9146  zneo  9176  nneoor  9177  zeo  9180  peano5uzti  9183  zindd  9193  uzp1  9383  uzaddcl  9408  supinfneg  9417  infsupneg  9418  supminfex  9419  ublbneg  9432  eqreznegel  9433  negm  9434  qmulz  9442  qnegcl  9455  irradd  9465  irrmul  9466  fzrev2  9896  negqmod0  10135  frec2uzuzd  10206  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  frecuzrdgsuctlem  10227  iseqovex  10260  seq3val  10262  seqvalcd  10263  seq3-1  10264  seqf  10265  seq3p1  10266  seqovcd  10267  seqp1cd  10270  seq3clss  10271  monoord  10280  monoord2  10281  ser3mono  10282  seq3split  10283  seq3caopr3  10285  seq3caopr2  10286  iseqf1olemjpcl  10299  iseqf1olemqpcl  10300  iseqf1olemfvp  10301  seq3f1olemqsumkj  10302  seq3f1olemqsum  10304  seq3f1oleml  10307  seq3f1o  10308  seq3homo  10314  seq3z  10315  seq3distr  10317  ser3ge0  10321  expp1  10331  expcllem  10335  expcl2lemap  10336  m1expcl2  10346  facnn  10505  fac0  10506  fac1  10507  faccl  10513  facdiv  10516  facndiv  10517  bccmpl  10532  bcn2  10542  bccl  10545  focdmex  10565  fihasheqf1oi  10566  seq3coll  10617  shftlem  10620  shftf  10634  seq3shft  10642  cjval  10649  cjth  10650  remim  10664  uzin2  10791  caubnd2  10921  negfi  11031  xrmaxltsup  11059  clim  11082  clim2  11084  climshftlemg  11103  climcn1  11109  climcn2  11110  iserex  11140  climub  11145  climserle  11146  climcau  11148  serf0  11153  sumfct  11175  sumrbdclem  11178  fsum3cvg  11179  summodclem3  11181  summodclem2a  11182  zsumdc  11185  fsumgcl  11187  fsum3  11188  fsumf1o  11191  isumss  11192  isumss2  11194  fsum3cvg2  11195  fsum3ser  11198  fsumcl2lem  11199  fsumsplitf  11209  sumpr  11214  sumtp  11215  fsumm1  11217  fsum1p  11219  isummulc2  11227  fsum2dlemstep  11235  fisumcom2  11239  fsumshftm  11246  fisum0diag2  11248  fsummulc2  11249  fsumge1  11262  fsum00  11263  fsumabs  11266  telfsumo  11267  telfsumo2  11268  fsumparts  11271  fsumrelem  11272  fsumiun  11278  binomlem  11284  isumshft  11291  isum1p  11293  isumrpcl  11295  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratnnlemseq  11327  cvgratnnlemabsle  11328  cvgratnnlemfm  11330  cvgratnnlemrate  11331  cvgratnn  11332  cvgratz  11333  mertenslem2  11337  mertensabs  11338  clim2prod  11340  prodfap0  11346  prodfrecap  11347  prodfdivap  11348  prodrbdclem  11372  fproddccvg  11373  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  zeo3  11601  mulsucdiv2z  11618  zob  11624  nn0o1gt2  11638  nno  11639  nn0o  11640  infssuzex  11678  infssuzcldc  11680  qnumdencl  11901  znnen  11947  ennnfonelemj0  11950  ennnfonelemg  11952  ennnfonelemom  11957  ctinfom  11977  ctiunctlemu1st  11983  ctiunctlemu2nd  11984  ctiunctlemudc  11986  ctiunctlemfo  11988  isstruct2im  12008  isstruct2r  12009  uniopn  12207  inopn  12209  fiinopn  12210  iscld  12311  iuncld  12323  tgrest  12377  iscn  12405  cnpval  12406  iscnp  12407  tgcn  12416  ssidcn  12418  lmbrf  12423  cnpnei  12427  cnima  12428  cnconst2  12441  cnrest2  12444  cnptopresti  12446  cnptoprest  12447  lmres  12456  lmtopcnp  12458  txbasval  12475  tx1cn  12477  tx2cn  12478  txcnp  12479  txcnmpt  12481  txdis1cn  12486  txlm  12487  cnmpt11  12491  cnmpt12  12495  cnmpt21  12499  cnmpt22  12502  ishmeo  12512  hmeoopn  12519  hmeocld  12520  qtopbasss  12729  fsumcncntop  12764  expcncf  12800  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemdisj  12826  ivthinclemloc  12827  ivthinc  12829  ivthdec  12830  limccl  12836  ellimc3apf  12837  cnmptlimc  12851  limccoap  12855  2irrexpq  13101  2irrexpqap  13103  bdinex1g  13270  bj-intexr  13277  bj-prexg  13280  bj-uniex  13286  bj-uniexg  13287  bdunexb  13289  bj-indsuc  13297  exmidsbthrlem  13392  qdencn  13397