Theorem eleq2i 1798

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 1795	. 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 162   = wceq 1136   e. wcel 1138

This theorem is referenced by:  eleq12i 1799  eleqtri 1806  eleq2s 1820  hbxfr 1829  abeq2i 1838  abeq1i 1839  rabeq2i 2124  elab2g 2239  elrabf 2246  elrab2 2249  cbvsbc 2312  elrabsf 2319  elabs2 2320  hbcsb1g 2400  hbcsbg 2402  dfnul2 2703  elsncgOLD 2888  eltp 2896  tpid3g 2937  elunirab 3012  elintrab 3050  exss 3331  elop 3343  opabidOLD 3373  brabg 3383  opelopabf 3387  elsuci 3546  elsucg 3547  elsuc2g 3548  sucidOLD 3559  suceloni 3705  elxp 3829  optocl 3872  opelcoOLD 3942  elcnv 3948  opelcnvgOLD 3952  opelres 4033  dfima2OLD 4077  rninxp 4166  dfco2aOLD 4206  fnopabg 4357  elfv 4490  nfvres 4516  dffv2 4545  fvopab3 4551  fvopab5 4567  fopabco 4616  fopabcos 4617  fopabap 4628  funfvima 4639  elunirn 4655  hboprd 4716  eloprabg 4747  1st2val 4849  2nd2val 4850  eloprabi 4871  fparlem3 4894  fparlem4 4895  fsplit 4897  tfrlem7 4936  tfrlem9 4938  tfr2 4944  rdgsucopabn 4966  tz7.48-2 4977  el1o 5002  oawordeulem 5047  ereldm 5154  0nelqs 5168  ecelqsdm 5169  ectocl 5172  ecoptocl 5173  brecop 5176  brecop2 5177  eceqopreq 5183  oprec 5188  elpm 5206  brsdom 5251  isfi 5252  enssdom 5253  brdom2 5258  map1 5300  pw2en 5316  brsdom2 5335  ordtypelem6 5499  onsdom 5504  zfregs 5563  en3lplem2 5566  r1tr 5574  tz9.12lem1 5579  tz9.12lem3 5581  rankr1 5594  rankel 5600  rankpw 5604  rankss 5608  rankun 5611  alephon 5672  elomsubsd 5681  aceq3lem 5690  aceq3 5691  aceq5lem2 5694  aceq5lem3 5695  aceq5lem4 5696  aceq5lem5 5697  ac6lem 5712  cardsdomel 5800  alephcard 5811  alephnbtwn 5812  alephnbtwn2 5813  alephord2 5820  alephval2 5846  cfub 5852  cardcf 5855  cflecard 5856  cfle 5857  elni 5952  ltpiord 5963  nlt1pi 5981  0npq 5998  0nsr 6136  opelcn 6196  opelreal 6197  elreal 6198  0ncn 6199  addcnsr 6201  mulcnsr 6202  hbnegd 6314  ltxr 6460  xrlenlt 6466  elxr 6502  peano2nn 6913  elnn0 7105  dfuzi 7209  elq 7232  elnnuz 7404  elnn0uz 7405  uzind4i 7418  uzrdgvali 7509  cardfz 7514  seq1lem1 7517  seq1suclem 7524  cvg1i 7967  cvg1 7968  facnn 7980  cbvsumi 8041  efcl 8369  infxpidmlem6 8621  infxpidmlem7 8622  infmap2lem1 8643  alephadd 8646  eltopsp 8668  tpsex 8669  istps 8670  subbas 8709  elcls3 8782  cnpco 8841  ismsg 8872  msflem 8875  blf 8916  lmle 9033  bcthlem4 9075  bcthlem14 9085  issubg 9220  ghgrpilem2 9237  isgalem 9244  isring 9260  ringi 9261  drngi 9288  vci 9294  isvclem 9323  isnvlem 9356  nvi 9360  vsfval 9381  vacnlem6 9467  isphg 9612  ishl 9731  sinq34lt0t 9853  efif1lem5 9883  efif1lem7 9885  shftefif1olem 9890  effoi 9894  eff1o 9897  oprabco 9953  istoset 10002  2txcn 10021  filrn 10085  elfilmap2 10105  elfilmap3 10106  fbaslim 10114  isexid 10156  smgrpismgm 10171  smgrpisass 10172  issmgrp 10173  mndissmgrp 10178  mndisexid 10179  ismnd 10182  uznzr 10208  isdivrng 10209  axhcompl 10292  dfhnorm2 10413  hhcmpl 10494  elch0 10551  chocunii 10597  omlsilem 10669  shsleji 10763  h1de2ctlem 10903  elspansni 10906  nonbooli 11023  spansncvi 11024  5oalem2 11027  3oalem2 11035  mayete3i 11100  mayete3OLDi 11101  hocoi 11119  adjeq 11288  cnlnssadj 11442  cnvbraval 11473  dfpjop 11547  pj3lem1 11571  cdj3lem3 11802  cdj3lem3b 11804  bnj13 12170  bnj15 12171  bnj25OLD 12185  bnj51 12218  bnj63 12224  bnj78 12231  bnj79OLD 12233  bnj100 12241  bnj99 12242  bnj112 12249  bnj136 12260  bnj158 12275  bnj168 12288  bnj529 12327  bnj566 12336  bnj883 12600  bnj923 12622  bnj922 12626  bnj952 12641  bnj1138 12728  bnj1144 12733  bnj1215 12783  bnj1454 12927  bnj1508 12960  bnj1509 12961  bnj594 13092  bnj580 13093  bnj916 13124  bnj983 13149  bnj984 13150  bnj1172 13232  bnj1174 13234  elfzm1b 13398  ghomgrpilem2 13421  eluznn0 13453  divides 13456  eucalgcvga 13546  eucalg 13547  mulgcdlem4 13551  3prm 13572  mpteqi 13631  dfon2lem3 13642  dfon2lem7 13646  elpred 13679  elpredg 13680  predel 13685  frsucopabn 13703  eltrcl 13724  trcltr 13728  xporderlem 13740  wfrlem5 13753  wfrlem9 13757  wfrlem11 13759  wfrlem12 13760  wfr2 13766  uninqs 14068  ficli 14081  domintref 14091  mlteqer 14109  fldleqt 14115  omslim2 14151  prmapcp2 14223  npincppr 14227  repcpwti 14229  dstr 14242  supaub 14339  suplub2 14340  geme2 14341  lteqtpos 14352  pospos 14360  tostos 14363  isdir2 14366  cbvprodi 14386  clfsebs 14430  symgfo 14453  gaplc 14454  com2i 14488  fldi 14499  zrfld 14507  zintdom 14510  vecval1b 14517  vecval3b 14518  muldisc 14547  vri 14557  bsi 14568  osneisi 14596  stoig2b 14625  subtopsin2 14626  fgsb 14635  conttnf 14658  dtt2 14665  bwt2 14674  singcon 14682  istopgrp 14685  topgrpi 14686  altretop 14707  cntrsetlem 14709  ismgra 14739  isalg 14750  algi 14756  isded 14765  dedi 14766  rdmob 14777  dmrngcmp 14780  iscat 14783  cati 14784  0ded 14786  0cat 14787  dualcat2lem 14811  dualded2lem 14812  dualded 14814  dualcat2 14815  ishoma 14818  idmon 14848  cinvlem3 14860  isfuna 14864  besubbeca 14878  idsubidsup 14887  idsubfun 14888  tarval1 14896  empistar 14901  ordtypelem6OLD 15062  onsdomOLD 15067  elomsubsdOLD 15076  opncldf1 15084  opncldf2 15085  opncldf3 15086  subcls 15106  compfipin0 15118  alexsub 15123  fnessref 15185  islocfin 15188  neibastop2lem1 15201  neibastop2lem2 15202  neibastop2lem3 15203  neibastop2lem4 15204  cnpfillim 15271  flimfbas 15283  fclusbas 15292  filnetlem1 15322  filnetlem3 15324  filnetlem4 15325  fnopabco 15393  upixp 15411  eroprlem 15414  eropreu 15415  eroprf 15417  indexfi 15437  pofun 15454  sdclem1 15491  fdc 15494  fsumltisumi 15505  caushft 15533  piececn 15576  txcnoprab 15593  txmet 15607  heiborlem14 15650  heiborlem24 15660  heiborlem30 15666  heiborlem35 15671  heiborlem37 15673  rrndstprj1 15699  rrndstprj2 15700  rrntotbndlem1 15702  rrntotbnd 15704  phtpycolem4 15736  phtpycolem5 15737  phtpyco 15738  pcocn 15758  pcohtpylem3 15764  pcohtpy 15765  flddivrng 15795  iscring 15827  fldcrng 15834  isdmn 15884  ishgrag 15973  hgralem 15974  issmo 16125  smores 16128  smores2 16129  smoge 16136  tpid3gVD 16325  en3lplem2VD 16327  elstr 16473  elstrscaf 16475  stbbi 16485  stb2xpl 16501  stb3xpl 16502  isposNEW 16532  isopos 16664  isolat 16691  isgrpNEW 16833  isringNEW 16871  issrng 16905  issdrng 16908  islvec 16917  isphil 16924

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1143  ax-17 1155  ax-4 1157  ax-5o 1159  ax-ext 1702

This theorem depends on definitions:  df-bi 163  df-an 241  df-ex 1165  df-cleq 1714  df-clel 1717

Copyright terms: Public domain