Theorem eleq2i 1609

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 1606	. 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 152   = wceq 1018   e. wcel 1020

This theorem is referenced by:  eleq12i 1610  eleqtri 1617  hbxfr 1634  abeq2i 1641  abeq1i 1642  rabeq2i 1887  elab2g 1978  elrabf 1982  elrab2 1985  elrabsf 2043  elabs2 2044  hbcsb1g 2107  hbcsbg 2109  dfnul2 2369  elsncg 2530  eltp 2539  elunirab 2619  elintrab 2651  exss 2887  elop 2899  opabid 2927  brabg 2935  opelopabf 2939  elsuci 3079  elsucg 3080  elsuc2g 3081  sucid 3091  rabxfr 3165  suceloni 3210  elxp 3323  optocl 3361  opelco 3418  elcnv 3424  opelcnvg 3427  opelres 3499  dfima2 3537  dfco2a 3640  fnopabg 3764  elfv 3875  nfvres 3901  dffv2 3926  fvopab3 3931  fvopab5 3947  fopabco 3989  fopabcos 3990  fopabap 3998  funfvima 4009  elunirn 4025  eloprabg 4110  1st2val 4201  2nd2val 4202  eloprabi 4223  fparlem3 4244  fparlem4 4245  fsplit 4247  tfrlem7 4261  tfrlem9 4263  tfr2 4269  rdgsucopabn 4291  tz7.48-2 4301  el1o 4325  oawordeulem 4367  ereldm 4468  0nelqs 4482  ecelqsdm 4483  ectocl 4486  ecoptocl 4487  brecop 4490  brecop2 4491  eceqopreq 4497  oprec 4502  elpm 4520  brsdom 4565  isfi 4566  enssdom 4567  brdom2 4572  map1 4614  pw2en 4630  brsdom2 4649  zfregs 4836  r1tr 4843  tz9.12lem1 4848  tz9.12lem3 4850  rankr1 4863  rankel 4869  rankpw 4873  rankss 4877  rankun 4880  aceq3lem 4921  aceq3 4922  aceq5lem2 4925  aceq5lem3 4926  aceq5lem4 4927  aceq5lem5 4928  ac6lem 4943  cardsdomel 5045  alephon 5058  alephcard 5060  alephnbtwn 5061  alephnbtwn2 5062  alephord2 5069  alephval2 5095  cfub 5101  cardcf 5104  cflecard 5105  cfle 5106  elni 5201  ltpiord 5212  nlt1pi 5230  0npq 5247  0nsr 5385  opelcn 5445  opelreal 5446  elreal 5447  0ncn 5448  addcnsr 5450  mulcnsr 5451  ltxr 5692  xrlenlt 5698  elxr 5732  peano2nn 6123  elnn0 6312  dfuzi 6416  elq 6439  elnnuz 6610  elnn0uz 6611  uzind4i 6624  uzrdgvali 6709  cardfz 6714  seq1lem1 6717  seq1suclem 6724  cvg1i 7166  cvg1 7167  facnn 7179  cbvsumi 7232  efcl 7560  infxpidmlem6 7812  infxpidmlem7 7813  infmap2lem1 7834  alephadd 7837  eltopsp 7859  tpsex 7860  istps 7861  subbas 7900  elcls3 7971  cnpco 8029  ismsg 8060  msflem 8063  blf 8104  lmle 8221  bcthlem4 8263  bcthlem14 8273  issubg 8408  ghgrpilem2 8425  isgalem 8432  isring 8448  ringi 8449  drngi 8474  vci 8480  isvclem 8509  isnvlem 8542  nvi 8546  vsfval 8567  vacnlem6 8653  isphg 8798  ishl 8917  sinq34lt0t 9042  efif1lem5 9072  efif1lem7 9074  shftefif1olem 9079  effoi 9083  eff1o 9086  axhcompl 9209  dfhnorm2 9330  hhcmpl 9411  elch0 9468  chocunii 9514  omlsilem 9586  shsleji 9680  h1de2ctlem 9820  elspansni 9823  nonbooli 9940  spansncvi 9941  5oalem2 9944  3oalem2 9952  mayete3i 10017  mayete3OLDi 10018  hocoi 10036  adjeq 10205  cnlnssadj 10358  cnvbraval 10389  dfpjop 10457  pj3lem1 10481  cdj3lem3 10713  cdj3lem3b 10715  ghomgrpilem2 10737  uninqs 10803  ficli 10821  domintref 10832  mlteqer 10854  fldleqt 10860  oprabco 10901  istoset 10967  lteqtpos 10986  pospos 10988  tostos 10989  isexid 10998  smgrpismgm 11014  smgrpisass 11015  issmgrp 11016  mndissmgrp 11027  mndisexid 11028  ismnd 11032  symgfo 11048  gaplc 11049  com2i 11063  uznzr 11091  isdivrng 11092  fldi 11098  zrfld 11106  zintdom 11109  vecval1 11116  vecval3 11117  vri 11122  bsi 11134  osneisi 11157  subtopsin2 11206  2txcn 11217  fgsb 11232  dtt2 11260  bwt2 11273  singcon 11287  istopgrp 11290  topgrpi 11291  altretop 11309  ismgra 11329  isalg 11340  algi 11346  isded 11355  dedi 11356  rdmob 11367  dmrngcmp 11370  iscat 11373  cati 11374  0ded 11376  0cat 11377  dualcat2lem 11401  dualded2lem 11402  dualded 11404  dualcat2 11405  ishoma 11408  idmon 11438  cinvlem3 11450  isfuna 11454  besubbeca 11468  idsubidsup 11477  idsubfun 11478  ordtypelem6 11568  onsdom 11573  elomsubsd 11582  opncldf1 11590  opncldf2 11591  opncldf3 11592  subcls 11617  compfipin0 11629  alexsub 11636  fnessref 11700  islocfin 11703  neibastop2lem1 11716  neibastop2lem2 11717  neibastop2lem3 11718  neibastop2lem4 11719  filrn 11779  fbaslim 11816  cnpfillim 11822  elfilmap2 11827  elfilmap3 11828  flimfbas 11849  fclusbas 11858  filnetlem1 11899  filnetlem3 11901  filnetlem4 11902  fnopabco 11923  upixp 11933  indexf 11957  sdclem1 11985  fsumltisumi 11996  caushft 12025  piececn 12064  txcnoprab 12079  heiborlem14 12121  heiborlem24 12131  heiborlem30 12137  heiborlem35 12142  heiborlem37 12144  rrndstprj 12170  rrndstprj2 12171  rrntotbndlem1 12173  rrntotbnd 12175  phtpyid 12188  phtpycolem4 12193  phtpycolem5 12194  phtpyco 12195  ishgrag 12292  hgralem 12293

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1025  ax-17 1033  ax-4 1035  ax-5o 1037  ax-ext 1528

This theorem depends on definitions:  df-bi 153  df-an 231  df-ex 1043  df-cleq 1539  df-clel 1542

Copyright terms: Public domain