Theorem eleq2i 1536

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 1533	. 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 955   e. wcel 957

This theorem is referenced by:  eleq12i 1537  eleqtr 1544  hbxfr 1561  abeq2i 1568  abeq1i 1569  rabeq2i 1807  elab2g 1897  elrabf 1901  elrab2 1904  elrabsf 1960  elabs2 1961  hbcsb1g 2021  hbcsbg 2023  dfnul2 2279  elsncg 2427  eltp 2436  elunirab 2510  elintrab 2541  exss 2765  elop 2779  opabid 2806  brabg 2814  rabxfr 2898  elsuci 3031  elsucg 3032  elsuc2g 3033  sucid 3047  suceloni 3058  elxp 3198  optocl 3231  opelco 3284  elcnv 3289  opelcnvg 3292  opelres 3368  dfima2 3401  fnopabg 3611  elfv 3717  nfvres 3743  fvopab3 3772  fvopab5 3788  fopabco 3827  fopabcos 3828  fopabap 3836  funfvima 3847  elunirn 3863  tfrlem7 3912  tfrlem9 3914  tfr2 3920  rdgsucopabn 3942  tz7.48-2 3952  eloprabg 4002  1st2val 4088  2nd2val 4089  eloprabi 4111  el1o 4139  oawordeulem 4181  ereldm 4278  0nelqs 4291  ecelqsdm 4292  ectocl 4295  ecoptocl 4296  brecop 4299  brecop2 4300  eceqopreq 4306  oprec 4311  elpm 4329  brsdom 4372  enssdom 4373  brdom2 4378  map1 4420  pw2en 4435  brsdom2 4450  zfregs 4630  r1tr 4637  tz9.12lem1 4642  tz9.12lem3 4644  rankr1 4657  rankel 4663  rankpw 4667  rankss 4671  rankun 4674  aceq3lem 4715  aceq3 4716  aceq5lem2 4719  aceq5lem3 4720  aceq5lem4 4721  aceq5lem5 4722  ac6lem 4737  cardsdomel 4835  alephon 4848  alephcard 4850  alephnbtwn 4851  alephnbtwn2 4852  alephord2 4859  alephval2 4885  cfub 4891  cardcf 4894  cflecard 4895  cfle 4896  elni 4987  ltpiord 4998  nlt1pi 5016  0npq 5033  0nsr 5171  opelcn 5231  opelreal 5232  elreal 5233  0ncn 5234  addcnsr 5236  mulcnsr 5237  ltxrt 5478  xrlenltt 5484  elxr 5518  peano2nn 5893  elnn0 6058  dfuz 6160  elq 6207  uzrdgval 6252  seq1lem1 6259  seq1suclem 6266  elnnuz 6385  elnn0uz 6386  uzind4i 6399  cvg1i 6872  cvg1 6873  facnnt 6885  cbvsum 6939  efclt 7271  infxpidmlem6 7517  infxpidmlem7 7518  infmap2lem1 7539  alephadd 7542  eltopsp 7564  tpsex 7565  istps 7566  subbas 7604  elcls3 7671  cnpco 7729  ismsg 7760  msflem 7763  blf 7806  lmle 7922  bcthlem4 7964  bcthlem14 7974  issubg 8080  ghgrpilem2 8098  isring 8105  ringi 8106  vci 8131  isvclem 8160  0vfval 8189  isnvlem 8193  nvi 8197  vsfval 8218  isphg 8435  ishl 8550  efif1lem5 8684  efif1lem7 8686  shftefif1olem 8696  effoi 8700  eff1o 8703  axhcompl 8823  dfhnorm2 8943  hhcmpl 9024  elch0 9081  chocuni 9127  omlsilem 9199  shslej 9293  h1de2ctlem 9434  elspansn 9437  nonbool 9553  spansncv 9554  5oalem2 9557  3oalem2 9565  mayete3 9630  hoco 9647  adjeqt 9816  cnlnssadj 9969  cnvbravalt 9999  dfpjopt 10067  pj3lem1 10090  cdj3lem3 10321  cdj3lem3b 10323  ghomgrpilem2 10342  uninqs 10400  ficli 10426  bsi 10441  fgsb 10503  dtt2 10534  ismgra 10558  isalg 10569  algi 10576  isded 10585  dedi 10586  rdmob 10597  iscat 10603  cati 10604  0ded 10606  0cat 10607  ishoma 10631  idmon 10660  isfuna 10664  ishgrag 10678  hgralem 10679

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-cleq 1468  df-clel 1471

Copyright terms: Public domain