Theorem eleq2i 2244

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

Syntax hints:   ↔ wb 105   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12i  2245  eleqtri  2252  eleq2s  2272  hbxfreq  2284  abeq2i  2288  abeq1i  2289  nfceqi  2315  raleqbii  2489  rexeqbii  2490  rabeq2i  2736  elab2g  2886  elrabf  2893  elrab3t  2894  elrab2  2898  cbvsbcw  2992  cbvsbc  2993  csbcow  3070  elin2  3325  dfnul2  3426  noel  3428  rabn0m  3452  rabeq0  3454  eltpg  3639  tpid3g  3709  oprcl  3804  elunirab  3824  elintrab  3858  exss  4229  elop  4233  opm  4236  brabsb  4263  brabga  4266  pofun  4314  elsuci  4405  elsucg  4406  elsuc2g  4407  ordsucim  4501  peano2  4596  elxp  4645  brab2a  4681  brab2ga  4703  elco  4795  elcnv  4806  dmmrnm  4848  elrnmptg  4881  opelres  4914  rninxp  5074  eliota  5206  funco  5258  elfv  5515  nfvres  5550  fvopab3g  5591  fvmptssdm  5602  fmptco  5684  funfvima  5750  fliftel  5796  acexmidlema  5868  acexmidlemb  5869  acexmidlem2  5874  eloprabga  5964  elrnmpo  5990  ovid  5993  offval  6092  xporderlem  6234  brtpos2  6254  issmo  6291  smores3  6296  tfrlem7  6320  tfrlem9  6322  tfr0dm  6325  tfri2  6369  rdgon  6389  freccllem  6405  frecfcllem  6407  frecsuclem  6409  el1o  6440  dif1o  6441  nnsucuniel  6498  elecg  6575  brecop  6627  erovlem  6629  oviec  6643  mapsncnv  6697  mptelixpg  6736  isfi  6763  enssdom  6764  map1  6814  xpcomco  6828  exmidpw  6910  exmidpweq  6911  fnfi  6938  fidcenumlemrks  6954  fidcenumlemrk  6955  djulclb  7056  eldju  7069  eldju2ndl  7073  eldju2ndr  7074  ctssdccl  7112  pw1nel3  7232  sucpw1nel3  7234  elni  7309  nlt1pig  7342  0nnq  7365  dfmq0qs  7430  dfplq0qs  7431  nqnq0  7442  elinp  7475  0npr  7484  ltdfpr  7507  nqprl  7552  nqpru  7553  addnqprlemfl  7560  addnqprlemfu  7561  mulnqprlemfl  7576  mulnqprlemfu  7577  cauappcvgprlemladdru  7657  suplocexprlemell  7714  addsrpr  7746  mulsrpr  7747  opelcn  7827  opelreal  7828  elreal  7829  elreal2  7831  0ncn  7832  addcnsr  7835  mulcnsr  7836  addvalex  7845  peano1nnnn  7853  peano2nnnn  7854  xrlenlt  8024  1nn  8932  peano2nn  8933  elnn0  9180  elnnne0  9192  un0addcl  9211  un0mulcl  9212  elxnn0  9243  uztrn2  9547  elnnuz  9566  elnn0uz  9567  elq  9624  elxr  9778  elfzm1b  10100  fz01or  10113  frecfzennn  10428  inftonninf  10443  seqf  10463  ser0  10516  ser0f  10517  hashinfom  10760  clim2ser  11347  clim2ser2  11348  isermulc2  11350  iserle  11352  climserle  11355  fsum3cvg3  11406  isumclim3  11433  isumadd  11441  sumsplitdc  11442  iserabs  11485  cvgcmpub  11486  isumshft  11500  isumsplit  11501  isumlessdc  11506  cvgratz  11542  cvgratgt0  11543  clim2prod  11549  clim2divap  11550  prodf1  11552  zproddc  11589  prodsnf  11602  divides  11798  dvdsflip  11859  infssuzex  11952  ialgrlemconst  12045  prm23lt5  12265  4sqlem2  12389  ennnfonelemjn  12405  ennnfonelem1  12410  ennnfonelemdm  12423  basmex  12523  istps  13617  lmss  13831  txuni2  13841  sinq34lt0t  14337  lgsdir2lem2  14515  2sqlem1  14546  bdceq  14679  bj-nntrans  14788  bj-nnelirr  14790  ss1oel2o  14828  trilpolemisumle  14871