Theorem eleq2i 2263

Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eleq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eleq2i	⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eleq2 2260	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)

Syntax hints:   ↔ wb 105   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleq12i  2264  eleqtri  2271  eleq2s  2291  hbxfreq  2303  abeq2i  2307  abeq1i  2308  nfceqi  2335  raleqbii  2509  rexeqbii  2510  rabeq2i  2760  elab2g  2911  elrabf  2918  elrab3t  2919  elrab2  2923  cbvsbcw  3017  cbvsbc  3018  csbcow  3095  elin2  3352  dfnul2  3453  noel  3455  rabn0m  3479  rabeq0  3481  eltpg  3668  tpid3g  3738  oprcl  3833  elunirab  3853  elintrab  3887  exss  4261  elop  4265  opm  4268  brabsb  4296  brabga  4299  pofun  4348  elsuci  4439  elsucg  4440  elsuc2g  4441  ordsucim  4537  peano2  4632  elxp  4681  brab2a  4717  brab2ga  4739  elco  4833  elcnv  4844  dmmrnm  4886  elrnmptg  4919  opelres  4952  rninxp  5114  eliota  5247  funco  5299  elfv  5559  nfvres  5595  fvopab3g  5637  fvmptssdm  5649  fmptco  5731  funfvima  5797  fliftel  5843  acexmidlema  5916  acexmidlemb  5917  acexmidlem2  5922  eloprabga  6013  elrnmpo  6040  ovid  6043  offval  6147  xporderlem  6298  brtpos2  6318  issmo  6355  smores3  6360  tfrlem7  6384  tfrlem9  6386  tfr0dm  6389  tfri2  6433  rdgon  6453  freccllem  6469  frecfcllem  6471  frecsuclem  6473  el1o  6504  dif1o  6505  nnsucuniel  6562  elecg  6641  brecop  6693  erovlem  6695  oviec  6709  mapsncnv  6763  mptelixpg  6802  isfi  6829  enssdom  6830  map1  6880  xpcomco  6894  exmidpw  6978  exmidpweq  6979  tpfidceq  7000  fnfi  7011  fidcenumlemrks  7028  fidcenumlemrk  7029  djulclb  7130  eldju  7143  eldju2ndl  7147  eldju2ndr  7148  ctssdccl  7186  pw1nel3  7316  sucpw1nel3  7318  elni  7394  nlt1pig  7427  0nnq  7450  dfmq0qs  7515  dfplq0qs  7516  nqnq0  7527  elinp  7560  0npr  7569  ltdfpr  7592  nqprl  7637  nqpru  7638  addnqprlemfl  7645  addnqprlemfu  7646  mulnqprlemfl  7661  mulnqprlemfu  7662  cauappcvgprlemladdru  7742  suplocexprlemell  7799  addsrpr  7831  mulsrpr  7832  opelcn  7912  opelreal  7913  elreal  7914  elreal2  7916  0ncn  7917  addcnsr  7920  mulcnsr  7921  addvalex  7930  peano1nnnn  7938  peano2nnnn  7939  xrlenlt  8110  1nn  9020  peano2nn  9021  elnn0  9270  elnnne0  9282  un0addcl  9301  un0mulcl  9302  elxnn0  9333  uztrn2  9638  elnnuz  9657  elnn0uz  9658  elq  9715  elxr  9870  elfzm1b  10192  fz01or  10205  infssuzex  10342  frecfzennn  10537  inftonninf  10553  seqf  10575  ser0  10644  ser0f  10645  hashinfom  10889  iswrd  10956  clim2ser  11521  clim2ser2  11522  isermulc2  11524  iserle  11526  climserle  11529  fsum3cvg3  11580  isumclim3  11607  isumadd  11615  sumsplitdc  11616  iserabs  11659  cvgcmpub  11660  isumshft  11674  isumsplit  11675  isumlessdc  11680  cvgratz  11716  cvgratgt0  11717  clim2prod  11723  clim2divap  11724  prodf1  11726  zproddc  11763  prodsnf  11776  divides  11973  dvdsflip  12035  nninfctlemfo  12234  ialgrlemconst  12238  prm23lt5  12459  4sqlem2  12585  4sqlem12  12598  ennnfonelemjn  12646  ennnfonelem1  12651  ennnfonelemdm  12664  basmex  12764  ghmeqker  13479  isrhm  13792  rrgmex  13895  lssmex  13989  lidlmex  14109  2idlmex  14135  df2idl2  14143  2idlss  14148  psrbagf  14304  istps  14376  lmss  14590  txuni2  14600  dvply1  15109  sinq34lt0t  15175  lgsdir2lem2  15378  gausslemma2dlem1a  15407  lgsquadlem1  15426  lgsquadlem2  15427  2sqlem1  15463  bdceq  15596  bj-nntrans  15705  bj-nnelirr  15707  ss1oel2o  15746  trilpolemisumle  15795