Theorem eleq1d 2208

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331   ∈ wcel 1480

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  eleq12d  2210  eqeltrd  2216  eqneltrd  2235  eqneltrrd  2236  rspcimdv  2790  rspcimedv  2791  reuind  2889  sbcel2g  3023  sbccsb2g  3032  breq1  3932  breq2  3933  inex1g  4064  intexr  4075  pwexg  4104  prexg  4133  opelopabsb  4182  pofun  4234  seex  4257  uniex  4359  uniexg  4361  unexb  4363  abnexg  4367  reusv3  4381  rabxfrd  4390  onun2  4406  onsucelsucexmid  4445  ordsucunielexmid  4446  dcextest  4495  tfisi  4501  peano2  4509  seinxp  4610  opabid2  4670  opeliunxp2  4679  elrn2g  4729  opeldm  4742  opeldmg  4744  elreldm  4765  elrn2  4781  opelresg  4826  elsnres  4856  iss  4865  elimasng  4907  issref  4921  rnxpid  4973  unielrel  5066  dffun5r  5135  funopg  5157  brprcneu  5414  tz6.12f  5450  fvelrnb  5469  ssimaex  5482  dmfco  5489  fvmpt3  5500  mptfvex  5506  fvmptf  5513  respreima  5548  fvelrn  5551  ffnfvf  5579  ffvresb  5583  fmptco  5586  fmptcof  5587  fsn  5592  fressnfv  5607  fnex  5642  funfvima  5649  funfvima3  5651  f1mpt  5672  fliftfuns  5699  isoselem  5721  ffnov  5875  fovcl  5876  ovmpos  5894  ov2gf  5895  ovg  5909  funimassov  5920  caovclg  5923  elovmpo  5971  off  5994  fnexALT  6011  fornex  6013  f1stres  6057  f2ndres  6058  xp1st  6063  xp2nd  6064  elxp6  6067  oprssdmm  6069  unielxp  6072  fmpox  6098  mpofvex  6101  opeliunxp2f  6135  dftpos4  6160  smoel  6197  tfrlem3-2d  6209  tfrlem8  6215  tfrlem9  6216  tfrlemibxssdm  6224  tfrlemi1  6229  tfrexlem  6231  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemaccex  6245  tfr1onlemres  6246  tfri1dALT  6248  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemaccex  6258  tfrcllemres  6259  tfrcl  6261  rdgtfr  6271  rdgon  6283  frecabex  6295  frecabcl  6296  frecfcllem  6301  frecsuclem  6303  nnacl  6376  nnmcl  6377  nnmordi  6412  nnaordex  6423  nnm00  6425  erexb  6454  qliftfuns  6513  ixpsnval  6595  elixp2  6596  resixp  6627  mptelixpg  6628  elixpsn  6629  fundmen  6700  fopwdom  6730  xpf1o  6738  dif1en  6773  diffitest  6781  diffifi  6788  inffiexmid  6800  unfiexmid  6806  unfidisj  6810  fiintim  6817  xpfi  6818  ssfirab  6822  fnfi  6825  iunfidisj  6834  snexxph  6838  fidcenumlemr  6843  elfi2  6860  ctssdccl  6996  isnumi  7038  addnidpig  7144  indpi  7150  dfplpq2  7162  addclnq  7183  mulclnq  7184  nnnq0lem1  7254  addclnq0  7259  mulclnq0  7260  nqpnq0nq  7261  distrnq0  7267  prloc  7299  prarloclemlo  7302  prarloclem3  7305  prarloclem5  7308  genpml  7325  genpmu  7326  addnqprl  7337  addnqpru  7338  mulnqprl  7376  mulnqpru  7377  ltexprlemell  7406  ltexprlemelu  7407  ltexprlemdisj  7414  ltexprlemloc  7415  ltexprlemrl  7418  ltexprlemru  7420  ltexpri  7421  recexprlemm  7432  recexprlemdisj  7438  recexprlemloc  7439  recexprlem1ssl  7441  recexprlem1ssu  7442  recexpr  7446  addclsr  7561  mulclsr  7562  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  suplocsr  7617  pitonn  7656  peano2nnnn  7661  axaddrcl  7673  axmulrcl  7675  peano5nnnn  7700  axpre-suploclemres  7709  negreb  8027  negf1o  8144  eqord1  8245  eqord2  8246  cju  8719  peano2nn  8732  nn1m1nn  8738  nnaddcl  8740  nnmulcl  8741  nnsub  8759  nndivtr  8762  un0addcl  9010  un0mulcl  9011  elnnnn0  9020  elz  9056  nnnegz  9057  znegclb  9087  zaddcllempos  9091  zaddcllemneg  9093  zaddcl  9094  nzadd  9106  zmulcl  9107  elz2  9122  zneo  9152  nneoor  9153  zeo  9156  peano5uzti  9159  zindd  9169  uzp1  9359  uzaddcl  9381  supinfneg  9390  infsupneg  9391  supminfex  9392  ublbneg  9405  eqreznegel  9406  negm  9407  qmulz  9415  qnegcl  9428  irradd  9438  irrmul  9439  fzrev2  9865  negqmod0  10104  frec2uzuzd  10175  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgg  10189  frecuzrdgsuctlem  10196  iseqovex  10229  seq3val  10231  seqvalcd  10232  seq3-1  10233  seqf  10234  seq3p1  10235  seqovcd  10236  seqp1cd  10239  seq3clss  10240  monoord  10249  monoord2  10250  ser3mono  10251  seq3split  10252  seq3caopr3  10254  seq3caopr2  10255  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  iseqf1olemfvp  10270  seq3f1olemqsumkj  10271  seq3f1olemqsum  10273  seq3f1oleml  10276  seq3f1o  10277  seq3homo  10283  seq3z  10284  seq3distr  10286  ser3ge0  10290  expp1  10300  expcllem  10304  expcl2lemap  10305  m1expcl2  10315  facnn  10473  fac0  10474  fac1  10475  faccl  10481  facdiv  10484  facndiv  10485  bccmpl  10500  bcn2  10510  bccl  10513  focdmex  10533  fihasheqf1oi  10534  seq3coll  10585  shftlem  10588  shftf  10602  seq3shft  10610  cjval  10617  cjth  10618  remim  10632  uzin2  10759  caubnd2  10889  negfi  10999  xrmaxltsup  11027  clim  11050  clim2  11052  climshftlemg  11071  climcn1  11077  climcn2  11078  iserex  11108  climub  11113  climserle  11114  climcau  11116  serf0  11121  sumfct  11143  sumrbdclem  11146  fsum3cvg  11147  summodclem3  11149  summodclem2a  11150  zsumdc  11153  fsumgcl  11155  fsum3  11156  fsumf1o  11159  isumss  11160  isumss2  11162  fsum3cvg2  11163  fsum3ser  11166  fsumcl2lem  11167  fsumsplitf  11177  sumpr  11182  sumtp  11183  fsumm1  11185  fsum1p  11187  isummulc2  11195  fsum2dlemstep  11203  fisumcom2  11207  fsumshftm  11214  fisum0diag2  11216  fsummulc2  11217  fsumge1  11230  fsum00  11231  fsumabs  11234  telfsumo  11235  telfsumo2  11236  fsumparts  11239  fsumrelem  11240  fsumiun  11246  binomlem  11252  isumshft  11259  isum1p  11261  isumrpcl  11263  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratnnlemseq  11295  cvgratnnlemabsle  11296  cvgratnnlemfm  11298  cvgratnnlemrate  11299  cvgratnn  11300  cvgratz  11301  mertenslem2  11305  mertensabs  11306  clim2prod  11308  prodfap0  11314  prodfrecap  11315  prodfdivap  11316  prodrbdclem  11340  fproddccvg  11341  prodmodclem3  11344  prodmodclem2a  11345  zeo3  11565  mulsucdiv2z  11582  zob  11588  nn0o1gt2  11602  nno  11603  nn0o  11604  infssuzex  11642  infssuzcldc  11644  qnumdencl  11865  znnen  11911  ennnfonelemj0  11914  ennnfonelemg  11916  ennnfonelemom  11921  ctinfom  11941  ctiunctlemu1st  11947  ctiunctlemu2nd  11948  ctiunctlemudc  11950  ctiunctlemfo  11952  isstruct2im  11969  isstruct2r  11970  uniopn  12168  inopn  12170  fiinopn  12171  iscld  12272  iuncld  12284  tgrest  12338  iscn  12366  cnpval  12367  iscnp  12368  tgcn  12377  ssidcn  12379  lmbrf  12384  cnpnei  12388  cnima  12389  cnconst2  12402  cnrest2  12405  cnptopresti  12407  cnptoprest  12408  lmres  12417  lmtopcnp  12419  txbasval  12436  tx1cn  12438  tx2cn  12439  txcnp  12440  txcnmpt  12442  txdis1cn  12447  txlm  12448  cnmpt11  12452  cnmpt12  12456  cnmpt21  12460  cnmpt22  12463  ishmeo  12473  hmeoopn  12480  hmeocld  12481  qtopbasss  12690  fsumcncntop  12725  expcncf  12761  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemdisj  12787  ivthinclemloc  12788  ivthinc  12790  ivthdec  12791  limccl  12797  ellimc3apf  12798  cnmptlimc  12812  limccoap  12816  bdinex1g  13099  bj-intexr  13106  bj-prexg  13109  bj-uniex  13115  bj-uniexg  13116  bdunexb  13118  bj-indsuc  13126  exmidsbthrlem  13217  qdencn  13222