Theorem eleq1 1534

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 1484	. . . 4 |- (A = B -> (x = A <-> x = B))
2	1	anbi1d 617	. . 3 |- (A = B -> ((x = A /\ x e. C) <-> (x = B /\ x e. C)))
3	2	exbidv 1279	. 2 |- (A = B -> (E.x(x = A /\ x e. C) <-> E.x(x = B /\ x e. C)))
4		df-clel 1472	. 2 |- (A e. C <-> E.x(x = A /\ x e. C))
5		df-clel 1472	. 2 |- (B e. C <-> E.x(x = B /\ x e. C))
6	3, 4, 5	3bitr4g 555	1 |- (A = B -> (A e. C <-> B e. C))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958  E.wex 980

This theorem is referenced by:  eleq12 1536  eleq1i 1537  eleq1d 1540  eleq1a 1543  cleqf 1560  nelneq 1561  hblem 1564  neleq1 1642  rgen2a 1699  ralcom2 1776  cbvralf 1796  cbvrexf 1797  cbvrex 1799  cbvreuv 1802  vtoclgaf 1851  rcla4 1871  rcla4e 1872  eqvinc 1883  ceqsrexv 1889  clel2 1891  elabgt 1895  elabf 1896  elabgf 1898  elrabf 1904  cbvrab 1910  abidhb 1912  moeq3 1921  mo2icl 1923  reu2 1930  reu3 1931  rmo4 1933  reu8 1936  ru 1938  dfsbcq 1943  sbc2or 1958  sbcel1gv 1980  hbsbc1gd 1983  hbsbcgd 1984  sbcralt 1990  sbcel12g 2011  sbceqdig 2012  csbiegft 2029  eldif 2057  dfss2f 2060  uniiunlem 2132  elun 2173  elin 2207  noel 2284  abn0 2290  disjne 2315  ifel 2379  ifcl 2380  elimel 2394  keepel 2399  elpw 2404  elpwg 2405  elpr2 2425  elsnc2g 2436  disjsn 2441  rabsn 2445  snssg 2463  prssg 2472  sssn 2473  eluni 2506  elunii 2508  eluniab 2513  elint 2539  elintg 2541  elinti 2542  elintab 2544  elintrabg 2546  intss1 2548  ssintab 2550  intab 2560  eliun 2570  eliin 2571  ssiun2s 2594  iunid 2603  opabss 2668  trel 2687  trss 2689  ssex 2719  intnex 2730  snex 2750  unipw 2756  elopab 2811  opelopab2 2819  epelc 2833  so 2864  reuuni2f 2883  rabxfr 2902  reuhyp 2905  reuunixfr 2906  elpwunsn 2912  efrirr 2928  tz7.2 2931  nordeq 2967  ordelord 2970  tz7.7 2973  onint0 3007  oneqmin 3018  onminex 3020  nsuceq0 3053  ordunisuc 3089  onsucuni2 3091  onuninsuc 3108  onun 3110  nlimsucg 3112  orduninsuc 3114  ordzsl 3116  onzsl 3117  limsssuc 3121  tfis 3127  elom 3134  elomg 3135  nnsuc 3148  peano5 3153  findes 3160  tfindes 3164  opelxp 3214  opelxpg 3216  ralxp 3218  opbrop 3238  onxpdisj 3241  ssrel 3247  ideqg 3276  opelxpex2 3279  eldm2g 3309  breldmg 3316  elreldm 3338  resiexg 3396  imai 3417  elimasng 3427  elxp4 3453  elxp5 3454  xpnz 3466  xpexr 3479  unielrel 3514  relcnvexb 3521  fneu 3592  fcoi2 3646  tz6.12i 3741  ndmfv 3745  fnopabfv 3758  fvelrnb 3760  funimass4 3763  fvelima 3764  fvelimab 3765  ssimaex 3768  fvopab3 3777  fvopab3ig 3778  fvopab4gf 3781  fvopabn 3786  fvopab2 3791  chfnrn 3802  fvelrn 3812  ffnfv 3828  abrexex 3860  elunirnALT 3869  tz7.48lem 3955  tz7.48-1 3956  tz7.49 3959  eloprabg 4007  resoprab 4009  oprabval 4023  oprabvalig 4024  oprabval2gf 4026  oprabval4g 4031  oprabval6g 4032  oprvalelrn 4039  oprssdm 4042  caoprmo 4070  2ndconst 4097  eqop 4104  unielxp 4107  elopabi 4117  eloprabi 4118  oalimcl 4194  oaass 4195  omlimcl 4209  odi 4210  nnaordex 4249  nnawordex 4250  ecelqsi 4292  ecelqsdm 4299  brecop 4306  eceqopreq 4313  th3qlem1 4314  dom2d 4404  mapsnen 4429  xpsnen 4435  pw2en 4446  xpmapenlem5 4500  limensuc 4507  php2 4514  ssnnfi 4535  ssnnfiOLD 4536  unblem1 4540  unblem2 4541  unfilem1 4548  fiint 4559  abfii2OLD 4562  supmo 4576  elirrv 4598  elirr 4599  sucprcreg 4600  en2lp 4602  inf0 4606  inf3lem6 4618  omelon 4629  noinfep 4640  setind 4648  tz9.12lem1 4659  tz9.12lem3 4661  tz9.13 4663  tz9.13g 4664  rankval 4668  rankvalg 4669  rankr1 4674  rankr1g 4675  r1pw 4686  r1pwcl 4687  rankonid 4695  rankr1id 4697  rankuni 4698  rankc2 4706  rankxpsuc 4715  scottex 4716  scott0 4717  aceq1 4729  aceq2 4731  aceq3lem 4732  aceq3 4733  aceq5lem1 4735  aceq5lem2 4736  aceq5lem3 4737  aceq5 4740  aceq6a 4741  aceq6b 4742  ac6lem 4754  ac6s4 4761  kmlem2 4766  kmlem4 4768  kmlem14 4778  kmlem15 4779  zorn2lem4 4791  zorn2lem5 4792  zorn2 4796  unidom 4808  oncard 4829  iscard 4853  iscard2 4854  carduni 4858  alephnbtwn 4868  alephle 4884  cardaleph 4885  iscard3 4888  alephsson 4894  alephval3 4903  cfsuc 4915  axpowndlem3 4951  ltpiord 5015  mulcanpi 5027  addnidpi 5028  indpi 5034  ltexpq 5080  ltexpq2 5081  nsmallpq 5083  ltbtwnpq 5084  prcdpq 5097  prub 5098  prnmax 5099  genpv 5102  genpprecl 5104  genpnmax 5110  distrlem5pr 5131  ltprord 5134  prlem934a 5137  prlem934 5139  ltaddpr2 5141  ltexprlem4 5145  ltexprlem6 5147  ltexprlem7 5148  ltexpri 5149  addcanpr 5152  prlem936 5155  reclem1pr 5156  recexpr 5160  supexpr 5163  negexsr 5211  recexsrlem 5212  recexsr 5216  suppsrlem 5221  suppsr 5222  suppsr2 5223  suppsr3 5224  supsrlem2 5226  supsrlem5 5229  supsrlem6 5230  supsr 5231  ltresr 5258  suprelem 5259  supre 5260  axrnegex 5283  axrrecex 5284  axcnre 5286  0cnALT 5350  1re 5435  ltxrltt 5500  ssxr 5540  mulcant 5690  mulcantOLD 5691  div11t 5765  recrect 5776  nnne0t 5949  sup2 6051  infm3 6054  infmsup 6068  nnunb 6070  elz 6137  elnn0z 6147  nn0subt 6161  elnn0nn 6171  peano5uzt 6204  uzindOLD 6208  elq 6257  qret 6259  om2uzran 6300  snunioolem 6414  uzind4s 6452  uzind4s2 6453  nnwof 6459  elfzp1 6510  fz1sbct 6517  limsupclt 6530  sqr0 6672  sqrlem20 6692  sqr2irrlem1 6724  negreb 6795  cjrebt 6800  nn0absclt 6879  bcpasc2t 6968  clim 6977  climshft 7104  climcmplem 7137  cvgcmp3cetlem1 7188  reccnv 7218  infcvgaux1 7219  infcvgaux2 7220  expcnvlem5 7231  expcnv 7233  geolim 7237  geolim1 7239  mulc1cncf 7279  efseq1ex 7306  absef01tlub 7388  eflegeot 7416  efm1legeot 7418  efcnlem4 7422  reeff1olem2 7425  acdc3 7487  acdc2 7490  acdc5 7493  acdc 7495  ruclem12 7521  eltopsp 7604  tpsex 7605  istps 7606  basis2t 7615  tg2t 7621  eltg3t 7626  subbas2OLD 7645  iscld3 7695  isopn3 7697  islp2 7747  cnpval 7759  cnpco 7769  cncnplem2 7775  cnconst 7780  hausnei 7784  sncld 7787  blin 7852  opni 7864  opnin 7869  lmbr 7928  iscaunns 7944  metelcls 7965  fsumcnlem 7989  bcthlem15 8013  bcth 8032  isgrp2i 8076  isring 8141  ringi 8142  vci 8167  isvclem 8196  nvvcop 8213  nmosetre 8427  blocni 8465  blocn 8467  isph 8481  siilem2 8512  spwmo 8656  spwpr3OLD 8662  circgrp 8740  effoi 8745  avril1 8784  normlem7tALT 8985  hlim 9056  hlim2 9060  closedsub 9093  chlim 9104  hlimcau 9107  ch2 9114  hhssnv 9134  hhsssh 9139  ocin 9169  chocuni 9172  pjeqt 9242  omlsilem 9244  omlsi 9245  dfch2 9249  pjch 9265  pjoc1t 9267  pjoc2t 9272  shslej 9338  shsidm 9357  shmods 9362  shjshsel 9416  spanun 9467  h1de2b 9477  h1de2ctlem 9478  h1de2ct 9479  elspansn2t 9490  spansnsst 9494  spanunsn 9502  cmbrt 9527  osumlem1 9578  osumlem7 9584  spansncv 9597  5oalem1 9599  3oalem1 9607  3oalem2 9608  pjch1t 9615  pjcht 9639  pjrn 9647  pjnelt 9671  eigret 9761  nmopsetretALT 9790  nmfnsetret 9804  hmopbdoptHIL 9913  elunop2t 9938  lnophmt 9944  lnopcont 9964  nmbdfnlbt 9979  lnfncont 9991  adjbd1o 10018  adjeq0 10024  bra11 10041  hmopidmcht 10081  hmopidmpjt 10082  pjssdif1 10103  elpjrncht 10118  pjclem4a 10126  pjcmmul2 10130  pj3lem1 10134  strlem1 10177  cvbrt 10209  mdbrt 10221  dmdbrt 10226  atom1d 10280  shatomistic 10288  atcvat2t 10316  irredt 10322  sumdmdi 10342  sumdmdlem 10345  cdjreu 10359  ghomgrplem 10389  cayleythlem 10413  uninqs 10441  elo 10444  infi1 10447  fine 10449  abfi 10451  fiiu 10453  fiiuOLD 10454  stcat 10457  cmpbva 10464  ficli 10472  fiv 10482  fivOLD 10483  fiiu2 10488  fiiu2OLD 10489  mapudiscn 10512  hmph 10524  hmphsyma 10528  hmphre 10530  hmphtr 10531  hmeogrp 10538  homcard 10539  fillsb 10560  filint 10562  fipfil2 10564  filintf 10569  fgsb 10570  fgsbOLD 10571  filint2 10574  infi 10578  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem2 10587  rcfpfillem3 10589  rcfpfillem4 10591  rcfpfillem5 10593  rcfpfillem6 10595  iint 10634  trran 10636  trnij 10637  cnvtr 10638  eloi 10659  rdmob 10681  ishomc 10717  ismonb 10738  isepib 10748

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain