Theorem eleq2i 1575

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 1572	. 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 144   = wceq 988   e. wcel 990

This theorem is referenced by:  eleq12i 1576  eleqtri 1583  hbxfr 1600  abeq2i 1607  abeq1i 1608  rabeq2i 1848  elab2g 1938  elrabf 1942  elrab2 1945  elrabsf 2003  elabs2 2004  hbcsb1g 2067  hbcsbg 2069  dfnul2 2326  elsncg 2475  eltp 2484  elunirab 2562  elintrab 2593  exss 2822  elop 2836  opabid 2863  brabg 2871  opelopabf 2875  rabxfr 2957  elsuci 3090  elsucg 3091  elsuc2g 3092  sucid 3106  suceloni 3117  elxp 3257  optocl 3294  opelco 3351  elcnv 3357  opelcnvg 3360  opelres 3432  dfima2 3468  dfco3OLD 3569  dfco2a 3570  dfco4OLD 3571  fnopabg 3690  elfv 3798  nfvres 3824  fvopab3 3853  fvopab5 3869  fopabco 3908  fopabcos 3909  fopabap 3917  funfvima 3928  elunirn 3944  tfrlem7 3993  tfrlem9 3995  tfr2 4001  rdgsucopabn 4023  tz7.48-2 4033  eloprabg 4084  1st2val 4175  2nd2val 4176  eloprabi 4198  el1o 4230  oawordeulem 4272  ereldm 4370  0nelqs 4385  ecelqsdm 4386  ectocl 4389  ecoptocl 4390  brecop 4393  brecop2 4394  eceqopreq 4400  oprec 4405  elpm 4423  brsdom 4468  isfi 4469  enssdom 4470  brdom2 4475  map1 4517  pw2en 4533  brsdom2 4548  zfregs 4733  r1tr 4740  tz9.12lem1 4745  tz9.12lem3 4747  rankr1 4760  rankel 4766  rankpw 4770  rankss 4774  rankun 4777  aceq3lem 4818  aceq3 4819  aceq5lem2 4822  aceq5lem3 4823  aceq5lem4 4824  aceq5lem5 4825  ac6lem 4840  cardsdomel 4941  alephon 4954  alephcard 4956  alephnbtwn 4957  alephnbtwn2 4958  alephord2 4965  alephval2 4991  cfub 4997  cardcf 5000  cflecard 5001  cfle 5002  elni 5093  ltpiord 5104  nlt1pi 5122  0npq 5139  0nsr 5277  opelcn 5337  opelreal 5338  elreal 5339  0ncn 5340  addcnsr 5342  mulcnsr 5343  ltxr 5584  xrlenlt 5590  elxr 5624  peano2nn 6022  elnn0 6211  dfuzi 6315  elq 6337  elnnuz 6500  elnn0uz 6501  uzind4i 6514  uzrdgvali 6595  seq1lem1 6602  seq1suclem 6609  cvg1i 7043  cvg1 7044  facnn 7056  cbvsumi 7109  efcl 7435  infxpidmlem6 7682  infxpidmlem7 7683  infmap2lem1 7704  alephadd 7707  eltopsp 7729  tpsex 7730  istps 7731  elcls3 7831  cnpco 7889  ismsg 7920  msflem 7923  blf 7964  lmle 8080  bcthlem4 8122  bcthlem14 8132  issubg 8235  ghgrpilem2 8253  isring 8260  ringi 8261  vci 8286  isvclem 8315  0vfval 8344  isnvlem 8348  nvi 8352  vsfval 8373  isphg 8595  ishl 8710  efif1lem5 8853  efif1lem7 8855  shftefif1olem 8860  effoi 8864  eff1o 8867  axhcompl 8987  dfhnorm2 9108  hhcmpl 9189  elch0 9246  chocunii 9292  omlsilem 9364  shsleji 9458  h1de2ctlem 9598  elspansni 9601  nonbooli 9716  spansncvi 9717  5oalem2 9720  3oalem2 9728  mayete3i 9793  hocoi 9810  adjeq 9977  cnlnssadj 10130  cnvbraval 10160  dfpjop 10228  pj3lem1 10252  cdj3lem3 10483  cdj3lem3b 10485  ghomgrpilem2 10507  uninqs 10563  uninqsOLD 10564  ficli 10590  domintref 10600  vri 10625  bsi 10631  fgsb 10708  dtt2 10742  ismgra 10777  isalg 10788  algi 10795  isded 10804  dedi 10805  rdmob 10816  iscat 10822  cati 10823  0ded 10825  0cat 10826  ishoma 10850  idmon 10880  cinvlem3 10892  isfuna 10896  ishgrag 10911  hgralem 10912

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-17 1003  ax-4 1005  ax-5o 1007  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1013  df-cleq 1505  df-clel 1508

Copyright terms: Public domain