Theorem eleq2i 1530

Description: Inference from equality to equivalence of membership.

Hypothesis

Ref	Expression
eleq1i.1	|- A = B

Assertion

Ref	Expression
eleq2i	|- (C e. A <-> C e. B)

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 |- A = B
2		eleq2 1527	. 2 |- (A = B -> (C e. A <-> C e. B))
3	1, 2	ax-mp 7	1 |- (C e. A <-> C e. B)

Syntax hints:   <-> wb 146   = wceq 953   e. wcel 955

This theorem is referenced by:  eleq12i 1531  eleqtr 1538  hbxfr 1555  abeq2i 1562  abeq1i 1563  rabeq2i 1801  elab2g 1891  elrabf 1895  elrab2 1898  elrabsf 1953  elabs2 1954  hbcsb1g 2014  hbcsbg 2016  dfnul2 2272  elsncg 2420  eltp 2429  elunirab 2504  elintrab 2535  exss 2759  elop 2773  opabid 2799  brabg 2807  rabxfr 2892  elsuci 3025  elsucg 3026  elsuc2g 3027  sucid 3041  suceloni 3052  elxp 3192  optocl 3225  opelco 3277  elcnv 3282  opelcnvg 3285  opelres 3356  dfima2 3389  fnopabg 3601  elfv 3707  nfvres 3733  fvopab3 3762  fvopab5 3778  fopabco 3817  fopabcos 3818  fopabap 3826  funfvima 3837  elunirn 3853  tfrlem7 3902  tfrlem9 3904  tfr2 3910  rdgsucopabn 3932  tz7.48-2 3942  eloprabg 3992  ndmoprgOLD 4029  1st2val 4079  2nd2val 4080  eloprabi 4102  el1o 4130  oawordeulem 4172  ereldm 4269  0nelqs 4282  ecelqsdm 4283  ectocl 4286  ecoptocl 4287  brecop 4290  brecop2 4291  eceqopreq 4297  oprec 4302  elpm 4320  brsdom 4363  enssdom 4364  brdom2 4369  map1 4411  pw2en 4426  brsdom2 4441  zfregs 4619  r1tr 4626  tz9.12lem1 4631  tz9.12lem3 4633  rankr1 4646  rankel 4652  rankpw 4656  rankss 4660  rankun 4663  aceq3lem 4704  aceq3 4705  aceq5lem2 4708  aceq5lem3 4709  aceq5lem4 4710  aceq5lem5 4711  ac6lem 4726  cardsdomel 4824  alephon 4837  alephcard 4839  alephnbtwn 4840  alephnbtwn2 4841  alephord2 4848  alephval2 4874  cfub 4880  cardcf 4883  cflecard 4884  cfle 4885  elni 4976  ltpiord 4987  nlt1pi 5005  0npq 5022  0nsr 5160  opelcn 5220  opelreal 5221  elreal 5222  0ncn 5223  addcnsr 5225  mulcnsr 5226  ltxrt 5467  xrlenltt 5473  elxr 5508  peano2nn 5883  elnn0 6048  dfuz 6150  elq 6195  uzrdgval 6239  seq1lem1 6246  seq1suclem 6253  elnnuz 6372  elnn0uz 6373  uzind4i 6386  cvg1i 6857  cvg1 6858  facnnt 6870  cbvsum 6924  efclt 7254  infxpidmlem6 7500  infxpidmlem7 7501  infmap2lem1 7521  alephadd 7524  eltopsp 7546  tpsex 7547  istps 7548  subbas 7586  elcls3 7652  cnpco 7708  ismsg 7739  msflem 7742  blf 7784  lmle 7895  bcthlem4 7936  bcthlem14 7946  issubg 8053  ghgrpilem2 8071  isring 8078  ringi 8079  vci 8104  isvcgOLD 8133  isvclem 8134  0vfval 8163  isnvlem 8167  isnvgOLD 8168  nvi 8173  vsfval 8194  isphg 8407  ishl 8522  efif1lem5 8649  efif1lem7 8651  shftefif1olem 8661  shftefif1olemOLD 8662  effoi 8666  effoiOLD 8667  eff1o 8670  dfhnorm2 8909  hhcmpl 8990  elch0 9047  chocuni 9088  omlsilem 9159  shslej 9253  h1de2ctlem 9394  elspansn 9397  nonbool 9513  spansncv 9514  5oalem2 9517  3oalem2 9525  mayete3 9590  hoco 9607  adjeqt 9775  cnlnssadj 9928  cnvbravalt 9956  dfpjopt 10021  pj3lem1 10044  cdj3lem3 10270  cdj3lem3b 10272  ghomgrpilem2 10291  uninqs 10342  ficli 10368  bsi 10382  fgsb 10444  dtt2 10462  ismgra 10486  isalg 10497  algi 10504  isded 10513  dedi 10514  rdmob 10525  iscat 10531  cati 10532  0ded 10534  0cat 10535  ishoma 10559  idmon 10588  isfuna 10592  ishgrag 10605  hgralem 10606

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465

Copyright terms: Public domain