Theorem eleq2i 2296

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

Syntax hints:   ↔ wb 105   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12i  2297  eleqtri  2304  eleq2s  2324  hbxfreq  2336  abeq2i  2340  abeq1i  2341  nfceqi  2368  raleqbii  2542  rexeqbii  2543  rabeq2i  2796  elab2g  2950  elrabf  2957  elrab3t  2958  elrab2  2962  cbvsbcw  3056  cbvsbc  3057  csbcow  3135  elin2  3392  dfnul2  3493  noel  3495  rabn0m  3519  rabeq0  3521  eltpg  3711  tpid3g  3781  oprcl  3880  elunirab  3900  elintrab  3934  exss  4312  elop  4316  opm  4319  brabsb  4348  brabga  4351  pofun  4402  elsuci  4493  elsucg  4494  elsuc2g  4495  ordsucim  4591  peano2  4686  elxp  4735  brab2a  4771  brab2ga  4793  elco  4887  elcnv  4898  dmmrnm  4942  elrnmptg  4975  opelres  5009  rninxp  5171  eliota  5305  funco  5357  elfv  5624  nfvres  5662  fvopab3g  5706  fvmptssdm  5718  fmptco  5800  funfvima  5870  fliftel  5916  acexmidlema  5991  acexmidlemb  5992  acexmidlem2  5997  eloprabga  6090  elrnmpo  6117  ovid  6120  offval  6224  xporderlem  6375  brtpos2  6395  issmo  6432  smores3  6437  tfrlem7  6461  tfrlem9  6463  tfr0dm  6466  tfri2  6510  rdgon  6530  freccllem  6546  frecfcllem  6548  frecsuclem  6550  el1o  6581  dif1o  6582  nnsucuniel  6639  elecg  6718  brecop  6770  erovlem  6772  oviec  6786  mapsncnv  6840  mptelixpg  6879  isfi  6910  enssdom  6911  map1  6963  xpcomco  6981  exmidpw  7066  exmidpweq  7067  tpfidceq  7088  fnfi  7099  fidcenumlemrks  7116  fidcenumlemrk  7117  djulclb  7218  eldju  7231  eldju2ndl  7235  eldju2ndr  7236  ctssdccl  7274  pw1nel3  7412  sucpw1nel3  7414  elni  7491  nlt1pig  7524  0nnq  7547  dfmq0qs  7612  dfplq0qs  7613  nqnq0  7624  elinp  7657  0npr  7666  ltdfpr  7689  nqprl  7734  nqpru  7735  addnqprlemfl  7742  addnqprlemfu  7743  mulnqprlemfl  7758  mulnqprlemfu  7759  cauappcvgprlemladdru  7839  suplocexprlemell  7896  addsrpr  7928  mulsrpr  7929  opelcn  8009  opelreal  8010  elreal  8011  elreal2  8013  0ncn  8014  addcnsr  8017  mulcnsr  8018  addvalex  8027  peano1nnnn  8035  peano2nnnn  8036  xrlenlt  8207  1nn  9117  peano2nn  9118  elnn0  9367  elnnne0  9379  un0addcl  9398  un0mulcl  9399  elxnn0  9430  uztrn2  9736  elnnuz  9755  elnn0uz  9756  elq  9813  elxr  9968  elfzm1b  10290  fz01or  10303  infssuzex  10448  frecfzennn  10643  inftonninf  10659  seqf  10681  ser0  10750  ser0f  10751  hashinfom  10995  iswrd  11068  pfxccatpfx1  11263  clim2ser  11843  clim2ser2  11844  isermulc2  11846  iserle  11848  climserle  11851  fsum3cvg3  11902  isumclim3  11929  isumadd  11937  sumsplitdc  11938  iserabs  11981  cvgcmpub  11982  isumshft  11996  isumsplit  11997  isumlessdc  12002  cvgratz  12038  cvgratgt0  12039  clim2prod  12045  clim2divap  12046  prodf1  12048  zproddc  12085  prodsnf  12098  divides  12295  dvdsflip  12357  nninfctlemfo  12556  ialgrlemconst  12560  prm23lt5  12781  4sqlem2  12907  4sqlem12  12920  ennnfonelemjn  12968  ennnfonelem1  12973  ennnfonelemdm  12986  basmex  13087  ghmeqker  13803  isrhm  14116  rrgmex  14219  lssmex  14313  lidlmex  14433  2idlmex  14459  df2idl2  14467  2idlss  14472  psrbagf  14628  istps  14700  lmss  14914  txuni2  14924  dvply1  15433  sinq34lt0t  15499  lgsdir2lem2  15702  gausslemma2dlem1a  15731  lgsquadlem1  15750  lgsquadlem2  15751  2sqlem1  15787  isuhgrm  15865  isushgrm  15866  isupgren  15889  isumgren  15899  umgredg  15937  umgrpredgv  15939  umgredgne  15942  umgredgnlp  15944  isuspgren  15949  isusgren  15950  ausgrusgrien  15963  usgredgppren  15989  edgssv2en  15991  uspgredg2vlem  16012  uspgredg2v  16013  ushgredgedg  16018  ushgredgedgloop  16020  bdceq  16163  bj-nntrans  16272  bj-nnelirr  16274  ss1oel2o  16313  trilpolemisumle  16365