Theorem eleq2i 2206

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

Syntax hints:   ↔ 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:  eleq12i  2207  eleqtri  2214  eleq2s  2234  hbxfreq  2246  abeq2i  2250  abeq1i  2251  nfceqi  2277  raleqbii  2447  rexeqbii  2448  rabeq2i  2683  elab2g  2831  elrabf  2838  elrab3t  2839  elrab2  2843  cbvsbcw  2936  cbvsbc  2937  elin2  3264  dfnul2  3365  noel  3367  rabn0m  3390  rabeq0  3392  eltpg  3569  tpid3g  3638  oprcl  3729  elunirab  3749  elintrab  3783  exss  4149  elop  4153  opm  4156  brabsb  4183  brabga  4186  pofun  4234  elsuci  4325  elsucg  4326  elsuc2g  4327  ordsucim  4416  peano2  4509  elxp  4556  brab2a  4592  brab2ga  4614  elco  4705  elcnv  4716  dmmrnm  4758  elrnmptg  4791  opelres  4824  rninxp  4982  funco  5163  elfv  5419  nfvres  5454  fvopab3g  5494  fvmptssdm  5505  fmptco  5586  funfvima  5649  fliftel  5694  acexmidlema  5765  acexmidlemb  5766  acexmidlem2  5771  eloprabga  5858  elrnmpo  5884  ovid  5887  offval  5989  xporderlem  6128  brtpos2  6148  issmo  6185  smores3  6190  tfrlem7  6214  tfrlem9  6216  tfr0dm  6219  tfri2  6263  rdgon  6283  freccllem  6299  frecfcllem  6301  frecsuclem  6303  el1o  6334  dif1o  6335  nnsucuniel  6391  elecg  6467  brecop  6519  erovlem  6521  oviec  6535  mapsncnv  6589  mptelixpg  6628  isfi  6655  enssdom  6656  map1  6706  xpcomco  6720  exmidpw  6802  fnfi  6825  fidcenumlemrks  6841  fidcenumlemrk  6842  djulclb  6940  eldju  6953  eldju2ndl  6957  eldju2ndr  6958  ctssdccl  6996  elni  7116  nlt1pig  7149  0nnq  7172  dfmq0qs  7237  dfplq0qs  7238  nqnq0  7249  elinp  7282  0npr  7291  ltdfpr  7314  nqprl  7359  nqpru  7360  addnqprlemfl  7367  addnqprlemfu  7368  mulnqprlemfl  7383  mulnqprlemfu  7384  cauappcvgprlemladdru  7464  suplocexprlemell  7521  addsrpr  7553  mulsrpr  7554  opelcn  7634  opelreal  7635  elreal  7636  elreal2  7638  0ncn  7639  addcnsr  7642  mulcnsr  7643  addvalex  7652  peano1nnnn  7660  peano2nnnn  7661  xrlenlt  7829  1nn  8731  peano2nn  8732  elnn0  8979  elnnne0  8991  un0addcl  9010  un0mulcl  9011  elxnn0  9042  uztrn2  9343  elnnuz  9362  elnn0uz  9363  elq  9414  elxr  9563  elfzm1b  9878  fz01or  9891  frecfzennn  10199  inftonninf  10214  seqf  10234  ser0  10287  ser0f  10288  hashinfom  10524  clim2ser  11106  clim2ser2  11107  isermulc2  11109  iserle  11111  climserle  11114  fsum3cvg3  11165  isumclim3  11192  isumadd  11200  sumsplitdc  11201  iserabs  11244  cvgcmpub  11245  isumshft  11259  isumsplit  11260  isumlessdc  11265  cvgratz  11301  cvgratgt0  11302  clim2prod  11308  clim2divap  11309  prodf1  11311  divides  11495  dvdsflip  11549  infssuzex  11642  ialgrlemconst  11724  ennnfonelemjn  11915  ennnfonelem1  11920  ennnfonelemdm  11933  istps  12199  lmss  12415  txuni2  12425  sinq34lt0t  12912  bdceq  13040  bj-nntrans  13149  bj-nnelirr  13151  ss1oel2o  13189  trilpolemisumle  13231