Theorem eleq1 1957

Description: Equality implies equivalence of membership.

Assertion

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

Proof of Theorem eleq1

Step	Hyp	Ref	Expression
1		eqeq2 1893	. . . 4 |- (A = B -> (x = A <-> x = B))
2	1	anbi1d 679	. . 3 |- (A = B -> ((x = A /\ x e. C) <-> (x = B /\ x e. C)))
3	2	exbidv 1657	. 2 |- (A = B -> (E.x(x = A /\ x e. C) <-> E.x(x = B /\ x e. C)))
4		df-clel 1880	. 2 |- (A e. C <-> E.x(x = A /\ x e. C))
5		df-clel 1880	. 2 |- (B e. C <-> E.x(x = B /\ x e. C))
6	3, 4, 5	3bitr4g 614	1 |- (A = B -> (A e. C <-> B e. C))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326

This theorem is referenced by:  eleq12 1959  eleq1i 1960  eleq1d 1963  eleq1a 1966  cleqf 1984  nelneq 1985  clelsb3 1990  clelsb3OLD 1991  hblemOLD 1994  neleq1 2101  rgen2a 2160  rgen2aOLD 2161  ralcom2 2244  ralcom2OLD 2245  cbvralf 2276  cbvrexf 2277  cbvreuv 2282  vtoclgaf 2350  vtoclgafOLD 2351  rcla4 2373  rcla4OLD 2374  rcla4e 2375  eqvincOLD 2388  ceqsrexv 2394  clel2 2396  elabgt 2400  elabgtOLD 2401  elabf 2402  elabgf 2404  elrabf 2413  ralrab 2418  cbvrab 2421  abidhb 2423  moeq3 2432  mo2icl 2434  reu2 2442  reu6 2443  rmo4 2445  reu8 2448  reuind 2450  ru 2451  dfsbcq 2455  sbc8g 2477  sbc2or 2481  sbcel1gv 2510  sbcel1gvOLD 2511  hbsbc1gd 2515  hbsbc1gdOLD 2516  hbsbcgd 2517  hbsbcgdOLD 2518  sbcralt 2527  sbcel12gOLD 2553  sbceqdigOLD 2555  csbiegft 2573  difjust 2595  unjust 2598  injust 2601  eldif 2609  dfss2f 2612  uniiunlem 2693  elun 2741  elin 2786  noel 2879  abn0 2892  disjne 2919  disjneOLD 2920  ifel 3006  ifcl 3007  elimel 3025  keepel 3030  elpw 3037  elpwg 3038  elpr2 3062  elsnc2g 3070  disjsnOLD 3090  rabsn 3094  tpid3g 3115  snssg 3124  difsn 3125  prssgOLD 3141  sssn 3142  eluni 3180  elunii 3182  eluniab 3189  elint 3220  elintg 3222  elinti 3223  elintiOLD 3224  elintab 3227  elintrabg 3229  intss1 3231  ssintab 3233  ssintabOLD 3234  intab 3247  uniintsn 3253  eliun 3259  eliin 3260  ssiun2s 3297  opabss 3397  opabssOLD 3398  trel 3418  trelOLD 3419  trss 3421  ssex 3455  intnex 3466  snexOLD 3493  opcom 3547  elopab 3559  opelopab2 3569  epelc 3584  so 3620  efrirr 3637  tz7.2 3639  nordeq 3677  ordelord 3680  tz7.7 3684  nsuceq0 3749  onun2i 3785  reuuni2f 3810  eufromeq4 3831  rabxfrd 3842  reuhypd 3848  reuunixfr 3850  elpwunsn 3856  onint0 3877  oneqmin 3886  onminex 3888  ordunisucOLD 3912  onsucuni2 3914  onsucuni2OLD 3915  onuninsuci 3921  nlimsucgOLD 3924  orduninsuc 3925  ordzsl 3927  onzsl 3928  onzslOLD 3929  limsssuc 3934  tfis 3938  tfindes 3946  elom 3952  elomg 3953  nnsuc 3969  peano5 3975  findes 3983  opelxp 4036  opelxpOLD 4037  opelxpg 4039  ralxp 4041  opbrop 4064  onxpdisj 4068  onxpdisjOLD 4069  ssrel 4075  ssrelOLD 4076  ssrelrel 4083  ssrelrelOLD 4084  ideqg 4114  ideqgOLD 4115  opelxpex2OLD 4120  eldm2g 4155  breldmg 4162  elreldm 4185  resiexg 4253  imai 4280  elimasng 4291  xpnz 4335  xpexr 4352  elxp4 4379  elxp5 4380  unielrel 4418  relcnvexb 4426  fneuOLD 4518  iunfopabOLD 4543  fcoi2OLD 4587  dmfex 4598  tz6.12i 4698  ndmfv 4702  dffn5 4717  fvelrnb 4719  funimass4 4722  fvelimaOLD 4724  fvelimab 4725  fvelimabOLD 4726  ssimaex 4729  fvopab3 4740  fvopab3ig 4741  fvopab4gf 4744  fvopabn 4749  fvopab2 4754  chfnrn 4775  fvelrn 4785  ffnfv 4801  abrexex 4836  elunirnALT 4845  eloprabg 4936  resoprab 4938  oprabval 4952  oprabvalig 4953  oprabval2gf 4955  oprabval4g 4960  oprabval4gALT 4961  oprabval6g 4962  oprvelrn 4969  oprssdm 4975  caoprmo 5003  cbvmpt 5011  eqop 5044  unielxp 5047  dfoprab4s 5056  dfoprab5sf 5058  elopabi 5059  eloprabi 5060  1stconst 5070  2ndconst 5071  reiota2f 5109  onopriun 5118  tz7.48lem 5164  tz7.48-1 5165  tz7.49 5168  oalimcl 5242  oaass 5243  omlimcl 5257  odi 5258  oeoa 5272  oeoe 5274  nnaordex 5306  nnawordex 5307  ecelqsdm 5358  brecop 5365  eceqopreq 5372  th3qlem1 5373  dom2d 5463  mapsnen 5488  fiprc 5492  xpsnen 5494  pw2en 5505  riotaundb 5574  riotaxfrd 5581  xpmapenlem5 5594  limensuc 5601  php2 5608  ssnnfi 5629  xpfi 5632  unblem1 5633  unblem2 5634  unfilem1 5641  unifi 5648  fiint 5650  abfii2 5652  abfii3 5653  abfii4 5654  iunfi 5659  supmo 5666  ordiso 5683  ordtypelem4 5687  ordtypelem5 5688  ordtypelem6 5689  ordtypelem7 5690  hartoglem 5692  elirrv 5700  elirrOLD 5702  sucprcreg 5703  en2lp 5707  inf0 5712  inf3lem6 5724  omelon 5736  noinfep 5747  setind 5759  tz9.12lem1 5770  tz9.12lem3 5772  tz9.13 5774  tz9.13g 5775  rankval 5779  rankvalg 5780  rankr1 5785  rankr1g 5786  r1pw 5797  r1pwcl 5798  rankonid 5806  rankr1id 5808  rankuni 5809  rankc2 5817  rankxpsuc 5826  scottex 5846  scott0 5847  aceq1 5891  aceq2 5893  aceq3lem 5894  aceq3 5895  aceq5lem1 5897  aceq5lem2 5898  aceq5lem3 5899  aceq5 5902  aceq6a 5903  aceq6b 5904  ac6lem 5916  ac6s4 5923  kmlem2 5928  kmlem4 5930  kmlem14 5940  kmlem15 5941  zorn2lem4 5953  zorn2lem5 5954  zorn2 5958  unidom 5970  oncard 5978  iscard 6005  iscard2 6006  carduni 6010  alephnbtwn 6016  alephle 6032  cardaleph 6033  iscard3 6036  alephsson 6042  alephval3 6051  cfsuc 6063  axpowndlem3 6103  ltpiord 6167  mulcanpi 6179  addnidpi 6180  indpi 6186  ltexpq 6232  ltexpq2 6233  nsmallpq 6235  ltbtwnpq 6236  prcdpq 6249  prub 6250  prnmax 6251  genpv 6254  genpprecl 6256  genpnmax 6262  distrlem5pr 6283  ltprord 6286  prlem934a 6289  prlem934 6291  ltaddpr2 6293  ltexprlem4 6297  ltexprlem6 6299  ltexprlem7 6300  ltexpri 6301  addcanpr 6304  prlem936 6307  reclem1pr 6308  recexpr 6312  supexpr 6315  negexsr 6363  recexsrlem 6364  recexsr 6368  suppsrlem 6373  suppsr 6374  suppsr2 6375  suppsr3 6376  supsrlem2 6378  supsrlem5 6381  supsrlem6 6382  supsr 6383  ltresr 6410  suprelem 6411  supre 6412  axrnegex 6436  axrrecex 6437  axcnre 6439  0cnALT 6504  1re 6598  ltxrlt 6669  renepnf 6708  renemnf 6710  ssxrOLD 6715  mulcan 6880  div11 6941  recrec 6952  nnne0 7132  sup2 7260  infm3 7263  infmsup 7277  nnunb 7279  elz 7346  elnn0z 7356  nn0sub 7370  elnn0nn 7380  peano5uzti 7416  uzindOLD 7420  zindd 7427  elq 7437  qre 7439  flidz 7476  snunioolem 7583  uzind4s 7621  uzind4s2 7622  nnwof 7628  fzsuc 7678  elfzp1 7683  fzsn 7684  fz1sbc 7696  om2uzrani 7711  limsupcl 7773  sqr0 7922  sqrlem20 7942  sqr2irrlem1 7974  negrebi 8045  cjreb 8050  nn0abscl 8131  bcpasc2 8220  clim 8237  climshfti 8364  climcmplem 8397  cvgcmp3cetlem1 8449  reccnv 8479  infcvgaux1i 8480  infcvgaux2i 8481  expcnvlem5 8492  expcnv 8494  geolim 8499  geolim1 8501  mulc1cncf 8541  efseq1ex 8568  absef01tlubi 8650  egt2OLD 8657  elt3OLD 8658  egt2lt3 8659  eflegeo 8681  efm1legeo 8683  efcnlem4 8687  reeff1olem2 8690  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  ruclem12 8790  eltopsp 8873  tpsex 8874  istps 8875  basis2 8884  tg2 8891  eltg3 8896  subbas 8914  subbas2 8915  iscld3 8971  isopn3 8973  islp2 9023  cnpval 9035  cnpco 9046  cncnplem2 9052  cnconst 9057  hausnei 9061  sncld 9064  blin 9129  opni 9141  opnin 9146  lmbr 9206  iscaunns 9222  metelcls 9243  fsumcnlem 9267  bcthlem15 9291  bcth 9310  isgrp2i 9360  isgalem 9449  ssga 9455  gapm 9462  isring 9465  ringi 9466  vci 9499  isvclem 9528  nvvcop 9545  vacnlem3 9669  vacnlem6 9672  nmosetre 9766  blocni 9805  blocn 9807  isph 9822  siilem2 9853  spwmo 9999  circgrp 10094  effoi 10099  axgroth6 10137  avril1 10142  oprabopabf 10157  dif1enOLD 10173  fipreima 10175  findcard 10178  findcardOLD 10179  fiv 10212  fine 10213  abfi 10215  fiiu2 10220  uptx 10226  txcn 10227  hmph 10241  subspid 10249  subtopmet 10256  fillsb 10270  fipfil2 10272  filintf 10274  infi 10280  fbunfip 10282  fgfil 10290  extbas1 10291  filrn 10293  limfil 10297  hausfillim 10303  flimopn 10321  cncomp 10331  usinuniop 10341  lpni 10347  unmnd 10405  fora2 10407  dvrunz 10419  normlem7tALT 10618  hlimi 10689  hlim2 10693  closedsub 10726  chlimi 10737  hlimcaui 10740  ch2 10747  hhssnv 10767  hhsssh 10772  ocin 10802  chocunii 10805  pjeq 10875  omlsilem 10877  omlsii 10878  dfch2 10882  pjchi 10898  pjoc1 10900  pjoc2 10905  shsleji 10971  shsidmi 10990  shmodsi 10995  shjshseli 11049  spanuni 11100  h1de2bi 11110  h1de2ctlem 11111  h1de2ci 11112  elspansn2 11123  spansnss 11127  spanunsni 11135  cmbr 11160  osumlem1 11213  osumlem7 11219  spansncvi 11232  5oalem1 11234  3oalem1 11242  3oalem2 11243  pjch1 11250  pjch 11274  pjrni 11282  pjnel 11306  eigre 11398  nmopsetretALT 11427  nmfnsetre 11441  hmopbdoptHIL 11550  elunop2 11575  lnophm 11581  lnopcon 11601  nmbdfnlb 11616  lnfncon 11628  adjbd1o 11655  adjeq0 11661  bra11 11679  hmopidmch 11725  hmopidmpj 11726  pjssdif1i 11747  elpjrnch 11763  pjclem4a 11771  pjcmmul2i 11775  pj3lem1 11779  strlem1 11822  cvbr 11854  mdbr 11866  dmdbr 11871  atom1d 11925  shatomistici 11933  atcvat2 11961  irred 11967  sumdmdii 11987  sumdmdlem 11990  cdjreui 12004  bnj36 12405  bnj100 12449  bnj99 12450  bnj116 12460  bnj142 12474  bnj144 12476  bnj521 12522  bnj898 12815  bnj919 12829  bnj924 12833  bnj1146 12943  bnj1185 12967  bnj1271 13030  bnj1306 13049  bnj1310 13050  bnj1377 13095  bnj1385 13102  bnj1401 13113  bnj1479 13155  bnj1484 13159  bnj1492 13161  bnj223 13252  bnj590 13298  bnj850 13312  bnj981 13356  bnj1014 13374  bnj1015 13375  bnj1112 13418  bnj1118 13420  bnj1123 13422  bnj1129 13425  bnj1128 13428  bnj1125 13430  bnj1137 13433  bnj1148 13434  bnj1152 13437  bnj1228 13456  bnj1287 13477  bnj1288 13478  bnj1326 13496  bnj1329 13497  bnj1321 13498  bnj1375 13509  bnj1376 13510  bnj1418 13529  bnj1417 13530  bnj1463 13550  bnj1491 13556  bnj1497 13560  elnn00nn 13602  ghomgrplem 13632  cayleythlem 13645  negn0 13655  divalglem8 13703  divalg 13706  gcdcllem3 13720  eucalgval 13749  1nprm 13769  isprm2 13775  3prm 13780  coprm 13782  untelirr 13796  untsucf 13798  elres 13824  epelcNEW 13826  frirrc 13833  fundmpss 13836  fvrn0 13837  dfon2lem3 13851  dfon2lem4 13852  dfon2lem5 13853  dfon2lem6 13854  dfon2lem7 13855  dfon2lem8 13856  dfon2lem9 13857  predbrg 13897  preddowncl 13907  wfisg 13917  frinsg 13941  xporderlem 13948  frxp 13951  poseq 13954  soseq 13955  wfrlem10 13966  sltval 13988  nosgnn0i 14000  axbday 14012  axdenselem3 14021  axdenselem8 14026  nocvxminlem 14028  nocvxmin 14029  axfelem12 14042  axfelem16 14046  axfelem17 14047  brbigcup 14074  elfix2 14078  elaltxp 14098  altopelaltxp 14099  fnoprvpop 14338  dfoprab4spop 14339  uninqs 14340  elo 14342  infi1 14343  fiiu 14344  stcat 14347  ficli 14353  vxveqv 14357  ref4w 14370  isunscov 14386  prj1 14395  eloi 14400  elintabg 14414  snelpwg 14415  celsor 14443  elixp2a 14493  elixp2b 14494  repcpwti 14503  unprj 14511  prl 14512  iscst2 14520  nZdef 14527  islatalg 14531  domrancur1b 14548  dupre2 14585  dupos2 14587  supdef 14604  defge3 14613  defse3 14614  inposet 14620  dutos2 14627  latdir 14643  hbprod 14660  clfsebs 14707  fincmpzer 14711  isppm 14715  grpdivfo 14737  fprodneg 14741  trran2 14757  cmprtr 14760  vecval1b 14794  vecval3b 14795  vri 14834  unint2t 14866  intfmu2 14867  mapdiscn 14871  mapudiscn 14872  hmphsyma 14882  hmphre 14884  hmphtr 14885  hmeogrp 14892  homcard 14893  subtopsin2 14907  ttcn 14913  istopx 14918  fgsb 14921  filint2 14923  cnfilca 14927  rcfpfillem2 14929  rcfpfillem3 14930  rcfpfillem4 14931  rcfpfillem5 14932  rcfpfillem6 14933  fbaslim2 14936  limfillem2 14939  limvinlv 14941  bwt2 14960  istopgrp 14971  topgrpi 14972  cntrsetlem 14999  iint 15012  trran 15014  trnij 15015  cnvtr 15016  lteqtpos 15024  supnuf 15041  rdmob 15095  dualalg 15131  ishomc 15138  ismonb 15159  isepib 15169  tarvalg 15213  tarval1g 15215  tarax3 15218  tarcrpr 15237  tclinf 15241  cptarc 15242  settrcon 15247  tarval2 15249  tarval2g 15250  bpmp 15251  btmp 15252  vtarsuelt 15272  fnctartar 15284  fnctartar2 15285  efp2 15290  isplibg0 15307  elfiun 15369  inficlALT 15372  ordisoOLD 15374  ordtypelem4OLD 15378  ordtypelem5OLD 15379  ordtypelem6OLD 15380  ordtypelem7OLD 15381  hartoglemOLD 15383  opncldf1 15402  opncldf2 15403  opncldf3 15404  cldbnd 15410  opnnei 15417  compsublem 15430  compsub 15431  hscptsscld 15434  compfipin0 15436  alexsublem3 15439  alexsublem4 15440  alexsub 15441  dfcon2 15442  cnconn 15444  reconnlem4 15449  1stcclb 15471  is2ndc2 15473  2ndc1stc 15477  2ndcctbss 15478  isfne3 15482  fnessex 15484  islocfin 15506  ptfinfin 15508  locfindsc 15515  comppfsc 15517  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  neibastop3 15524  fnemeet1 15528  t0dist 15541  ist1-3 15543  t1sep 15546  regsep 15550  fbasfip 15556  filfinnfr 15561  isufil2 15565  ufilss 15567  filssufillem 15570  ufileu 15573  uffixfr 15575  fixufil 15576  ufinffr 15578  ufilen 15579  filcon 15580  limfilcf 15587  flimcls 15588  rnelfmlem 15592  rnelfm 15593  fmfnfmlem2 15595  fmfnfmlem4 15597  fmfnfm 15598  sfcls 15604  filclus 15605  isfclus 15606  fcluscf 15612  flimfcls 15613  flimfnfcls 15615  fcluscomp 15621  tailf 15633  istail 15634  tailmap 15636  tailuni 15638  filnetlem1 15640  filnetlem2 15641  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  filnet 15645  morex 15662  ralrabOLD 15670  oprabvalg 15706  oprabval2a 15707  f1elima 15719  fimaxg 15747  fipreimaOLD 15756  inficl 15757  fzfi2 15787  elfzp12 15795  fzm1 15796  absz 15797  sdc 15811  fdc 15812  fdc1 15813  fsumltisum 15824  fsumleisum 15827  fsumlt1 15831  trirn 15834  subspcld2 15839  neificl 15841  mettrifi 15847  oprpiece1res2 15881  cncfres 15895  tlmbr 15904  txsubsp 15912  cnresoprab 15915  cnopropabco 15917  cnoproprabco 15919  cnoprab1 15921  cnoprab2 15922  txmet 15925  totbndbnd 15944  ismtyhmeolem 15950  heiborlem1 15955  heiborlem7 15961  heiborlem10 15964  heiborlem11 15965  heiborlem15 15969  heiborlem18 15972  heiborlem28 15982  heiborlem29 15983  heiborlem30 15984  heiborlem35 15989  heiborlem41 15995  heiborlem42 15996  bfplem3 16000  bfplem8 16005  bfp 16009  reheibor 16025  grpkerinj 16042  isphtpc 16059  pcoval 16073  pcorev 16087  pi1bval 16088  isdivrng1 16109  isriscg 16138  risci 16141  iscring2 16146  iscringd 16147  0ring 16175  divrngidl 16176  igenval 16209  igenval2 16214  prnc 16215  pridlc 16219  prtlem90 16246  rcla4t 16407  smoel 16451  smoge 16454  tpid3gVD 16666  eustrdif 16722  isopos 16909  glbcon 17028  isringNEW 17142  issrng 17176  islvec 17188  isphil 17195  isline 17220  ispoint 17223  psubspi 17228  pmapglb 17252  polval2 17319  osumcllem4 17367  pexmidlem1 17378

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-cleq 1877  df-clel 1880

Copyright terms: Public domain