Theorem eleq1 1577

Description: Equality implies equivalence of membership.

Assertion

Ref	Expression
eleq1	⊢ (A = B → (A ∈ C ↔ B ∈ C))

Proof of Theorem eleq1

Step	Hyp	Ref	Expression
1		eqeq2 1527	. . . 4 ⊢ (A = B → (x = A ↔ x = B))
2	1	anbi1d 620	. . 3 ⊢ (A = B → ((x = A ⋀ x ∈ C) ↔ (x = B ⋀ x ∈ C)))
3	2	exbidv 1317	. 2 ⊢ (A = B → (∃x(x = A ⋀ x ∈ C) ↔ ∃x(x = B ⋀ x ∈ C)))
4		df-clel 1514	. 2 ⊢ (A ∈ C ↔ ∃x(x = A ⋀ x ∈ C))
5		df-clel 1514	. 2 ⊢ (B ∈ C ↔ ∃x(x = B ⋀ x ∈ C))
6	3, 4, 5	3bitr4g 558	1 ⊢ (A = B → (A ∈ C ↔ B ∈ C))

Syntax hints:   → wi 3   ↔ wb 144   ⋀ wa 221   = wceq 992   ∈ wcel 994  ∃wex 1016

This theorem is referenced by:  eleq12 1579  eleq1i 1580  eleq1d 1583  eleq1a 1586  cleqf 1603  nelneq 1604  hblem 1607  neleq1 1688  rgen2a 1745  ralcom2 1822  cbvralf 1842  cbvrexf 1843  cbvrex 1845  cbvreuv 1848  vtoclgaf 1897  rcla4 1917  rcla4e 1918  eqvinc 1929  ceqsrexv 1935  clel2 1937  elabgt 1941  elabf 1942  elabgf 1944  elrabf 1950  cbvrab 1956  abidhb 1958  moeq3 1967  mo2icl 1969  reu2 1976  reu3 1977  rmo4 1979  reu8 1982  ru 1984  dfsbcq 1988  sbc2or 2006  sbcel1gv 2028  hbsbc1gd 2031  hbsbcgd 2032  sbcralt 2040  sbcel12g 2062  sbceqdig 2063  csbiegft 2081  eldif 2109  dfss2f 2112  uniiunlem 2184  elun 2225  elin 2259  noel 2336  abn0 2343  disjne 2368  ifel 2433  ifcl 2434  elimel 2451  keepel 2456  elpw 2461  elpwg 2462  elpr2 2483  elsnc2g 2497  disjsn 2502  rabsn 2506  snssg 2527  prssg 2537  sssn 2538  eluni 2572  elunii 2574  eluniab 2579  elint 2606  elintg 2608  elinti 2609  elintab 2611  elintrabg 2613  intss1 2615  ssintab 2617  intab 2627  eliun 2637  eliin 2638  ssiun2s 2662  opabss 2742  trel 2761  trss 2763  ssex 2793  intnex 2804  snex 2826  opcom 2877  elopab 2888  opelopab2 2896  epelc 2911  so 2943  efrirr 2957  tz7.2 2959  nordeq 2994  ordelord 2997  tz7.7 3001  nsuceq0 3053  onun2i 3085  reuuni2f 3107  rabxfr 3125  reuhyp 3128  reuunixfr 3129  elpwunsn 3135  onint0 3153  oneqmin 3162  onminex 3164  ordunisuc 3186  onsucuni2 3188  onuninsuci 3194  nlimsucg 3196  orduninsuc 3197  ordzsl 3199  onzsl 3200  limsssuc 3204  tfis 3208  tfindes 3215  elom 3221  elomg 3222  nnsuc 3235  peano5 3241  findes 3248  opelxp 3297  opelxpg 3299  ralxp 3301  opbrop 3324  onxpdisj 3328  ssrel 3334  ssrelrel 3340  ideqg 3366  opelxpex2 3369  eldm2g 3400  breldmg 3407  elreldm 3425  resiexg 3486  imai 3509  elimasng 3519  xpnz 3551  xpexr 3564  elxp4 3585  elxp5 3586  unielrel 3619  relcnvexb 3626  fneu 3698  iunfopab 3719  fcoi2 3753  tz6.12i 3852  ndmfv 3856  dffn5 3869  fvelrnb 3871  funimass4 3874  fvelima 3875  fvelimab 3876  ssimaex 3879  fvopab3 3888  fvopab3ig 3889  fvopab4gf 3892  fvopabn 3897  fvopab2 3902  chfnrn 3916  fvelrn 3926  ffnfv 3942  abrexex 3974  elunirnALT 3983  eloprabg 4067  resoprab 4069  oprabval 4083  oprabvalig 4084  oprabval2gf 4086  oprabval4g 4091  oprabval4gALT 4092  oprabval6g 4093  oprvelrn 4100  oprssdm 4103  caoprmo 4131  eqop 4164  unielxp 4167  dfoprab4s 4176  dfoprab5sf 4178  elopabi 4179  eloprabi 4180  1stconst 4190  2ndconst 4191  onopriun 4211  tz7.48lem 4256  tz7.48-1 4257  tz7.49 4260  oalimcl 4330  oaass 4331  omlimcl 4345  odi 4346  oeoa 4360  oeoe 4362  nnaordex 4389  nnawordex 4390  ecelqsdm 4440  brecop 4447  eceqopreq 4454  th3qlem1 4455  dom2d 4545  mapsnen 4570  fiprc 4574  xpsnen 4576  pw2en 4587  xpmapenlem5 4647  limensuc 4654  php2 4661  ssnnfi 4682  xpfi 4685  unblem1 4686  unblem2 4687  unfilem1 4694  unifi 4701  fiint 4703  abfii2 4705  abfii3 4706  abfii4 4707  iunfi 4712  supmo 4719  elirrv 4741  elirr 4742  sucprcreg 4743  en2lp 4747  inf0 4751  inf3lem6 4763  omelon 4775  noinfep 4786  setind 4794  tz9.12lem1 4805  tz9.12lem3 4807  tz9.13 4809  tz9.13g 4810  rankval 4814  rankvalg 4815  rankr1 4820  rankr1g 4821  r1pw 4832  r1pwcl 4833  rankonid 4841  rankr1id 4843  rankuni 4844  rankc2 4852  rankxpsuc 4861  scottex 4862  scott0 4863  aceq1 4875  aceq2 4877  aceq3lem 4878  aceq3 4879  aceq5lem1 4881  aceq5lem2 4882  aceq5lem3 4883  aceq5 4886  aceq6a 4887  aceq6b 4888  ac6lem 4900  ac6s4 4907  kmlem2 4912  kmlem4 4914  kmlem14 4924  kmlem15 4925  zorn2lem4 4937  zorn2lem5 4938  zorn2 4942  unidom 4954  oncard 4976  iscard 5003  iscard2 5004  carduni 5008  alephnbtwn 5018  alephle 5034  cardaleph 5035  iscard3 5038  alephsson 5044  alephval3 5053  cfsuc 5065  axpowndlem3 5105  ltpiord 5169  mulcanpi 5181  addnidpi 5182  indpi 5188  ltexpq 5234  ltexpq2 5235  nsmallpq 5237  ltbtwnpq 5238  prcdpq 5251  prub 5252  prnmax 5253  genpv 5256  genpprecl 5258  genpnmax 5264  distrlem5pr 5285  ltprord 5288  prlem934a 5291  prlem934 5293  ltaddpr2 5295  ltexprlem4 5299  ltexprlem6 5301  ltexprlem7 5302  ltexpri 5303  addcanpr 5306  prlem936 5309  reclem1pr 5310  recexpr 5314  supexpr 5317  negexsr 5365  recexsrlem 5366  recexsr 5370  suppsrlem 5375  suppsr 5376  suppsr2 5377  suppsr3 5378  supsrlem2 5380  supsrlem5 5383  supsrlem6 5384  supsr 5385  ltresr 5412  suprelem 5413  supre 5414  axrnegex 5437  axrrecex 5438  axcnre 5440  0cnALT 5504  1re 5589  ltxrlt 5654  ssxr 5694  mulcan 5844  div11 5904  recrec 5915  nnne0 6094  sup2 6219  infm3 6222  infmsup 6236  nnunb 6238  elz 6305  elnn0z 6315  nn0sub 6329  elnn0nn 6339  peano5uzti 6375  uzindOLD 6379  zindd 6386  elq 6396  qre 6398  flidz 6435  snunioolem 6541  uzind4s 6579  uzind4s2 6580  nnwof 6586  fzsuc 6636  elfzp1 6641  fz1sbc 6648  om2uzrani 6663  limsupcl 6725  sqr0 6873  sqrlem20 6893  sqr2irrlem1 6925  negrebi 6996  cjreb 7001  nn0abscl 7082  bcpasc2 7171  clim 7180  climshfti 7307  climcmplem 7340  cvgcmp3cetlem1 7392  reccnv 7422  infcvgaux1i 7423  infcvgaux2i 7424  expcnvlem5 7435  expcnv 7437  geolim 7442  geolim1 7444  mulc1cncf 7484  efseq1ex 7511  absef01tlubi 7593  egt2OLD 7600  elt3OLD 7601  egt2lt3 7602  eflegeo 7624  efm1legeo 7626  efcnlem4 7630  reeff1olem2 7633  acdc3 7698  acdc2 7702  acdc5 7705  acdc 7707  ruclem12 7733  eltopsp 7816  tpsex 7817  istps 7818  basis2 7827  tg2 7833  eltg3 7838  subbas 7856  subbas2 7857  iscld3 7905  isopn3 7907  islp2 7957  cnpval 7969  cnpco 7979  cncnplem2 7985  cnconst 7990  hausnei 7994  sncld 7997  blin 8062  opni 8074  opnin 8079  lmbr 8139  iscaunns 8155  metelcls 8176  fsumcnlem 8200  bcthlem15 8224  bcth 8243  isgrp2i 8293  isring 8382  ringi 8383  vci 8414  isvclem 8443  nvvcop 8460  vacnlem3 8584  vacnlem6 8587  nmosetre 8681  blocni 8720  blocn 8722  isph 8737  siilem2 8768  spwmo 8918  circgrp 9012  effoi 9017  avril1 9058  normlem7tALT 9261  hlimi 9332  hlim2 9336  closedsub 9369  chlimi 9380  hlimcaui 9383  ch2 9390  hhssnv 9410  hhsssh 9415  ocin 9445  chocunii 9448  pjeq 9518  omlsilem 9520  omlsii 9521  dfch2 9525  pjchi 9541  pjoc1 9543  pjoc2 9548  shsleji 9614  shsidmi 9633  shmodsi 9638  shjshseli 9692  spanuni 9743  h1de2bi 9753  h1de2ctlem 9754  h1de2ci 9755  elspansn2 9766  spansnss 9770  spanunsni 9778  cmbr 9803  osumlem1 9856  osumlem7 9862  spansncvi 9875  5oalem1 9877  3oalem1 9885  3oalem2 9886  pjch1 9893  pjch 9917  pjrni 9925  pjnel 9949  eigre 10041  nmopsetretALT 10070  nmfnsetre 10084  hmopbdoptHIL 10192  elunop2 10217  lnophm 10223  lnopcon 10243  nmbdfnlb 10258  lnfncon 10270  adjbd1o 10297  adjeq0 10303  bra11 10321  hmopidmch 10361  hmopidmpj 10362  pjssdif1i 10383  elpjrnch 10399  pjclem4a 10407  pjcmmul2i 10411  pj3lem1 10415  strlem1 10458  cvbr 10490  mdbr 10502  dmdbr 10507  atom1d 10561  shatomistici 10569  atcvat2 10598  irred 10604  sumdmdii 10624  sumdmdlem 10627  cdjreui 10641  ghomgrplem 10674  cayleythlem 10698  uninqs 10730  elo 10733  infi1 10735  fine 10736  abfi 10737  fiiu 10738  stcat 10741  cmpbva 10748  ficli 10756  vxveqv 10761  ref3w 10772  isunscov 10796  prj1 10809  eloi 10817  islatalg 10831  fiv 10849  fiiu2 10852  infi 10854  inposet 10868  dupos2 10879  lteqtpos 10880  isppm 10917  unmnd 10951  fora2 10953  dvrunz 10970  vri 10981  mapudiscn 11015  hmph 11030  hmphsyma 11034  hmphre 11036  hmphtr 11037  hmeogrp 11044  homcard 11045  subtopsin2 11067  fillsb 11073  fipfil2 11077  filintf 11081  fgsb 11082  filint2 11084  cnfilca 11088  rcfpfillem2 11090  rcfpfillem3 11091  rcfpfillem4 11092  rcfpfillem5 11093  rcfpfillem6 11094  limfillem2 11102  bwt2 11123  usinuniop 11128  iint 11157  trran 11159  trnij 11160  cnvtr 11161  rdmob 11202  ishomc 11244  ismonb 11265  isepib 11275  efp2 11321  xpss1 11403  xpss2 11404  lpni 11417  elfiun 11421  inficlALT 11424  ordiso 11426  ordtypelem4 11430  ordtypelem5 11431  ordtypelem6 11432  ordtypelem7 11433  hartoglem 11435  opncldf1 11454  opncldf2 11455  opncldf3 11456  cldbnd 11462  opnnei 11469  subspid 11478  compsublem 11487  compsub 11488  hscptsscld 11491  compfipin0 11493  cncomp 11494  alexsublem3 11498  alexsublem4 11499  alexsub 11500  dfcon2 11501  cnconn 11503  subtopmet 11506  reconnlem4 11510  1stcclb 11532  is2ndc2 11534  2ndc1stc 11538  2ndcctbss 11539  isfne3 11543  fnessex 11545  islocfin 11567  ptfinfin 11569  locfindsc 11576  comppfsc 11578  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  neibastop3 11585  fnemeet1 11589  t0dist 11602  ist1-3 11604  t1sep 11607  regsep 11611  fbasfip 11627  fbunfip 11631  fgfil 11638  extbas1 11641  filrn 11643  filfinnfr 11646  isufil2 11650  ufilss 11652  filssufillem 11655  ufileu 11658  uffixfr 11660  fixufil 11661  ufinffr 11663  ufilen 11664  filcon 11665  limfil 11675  flimopn 11679  limfilcf 11683  flimcls 11684  hausfillim 11685  rnelfmlem 11698  rnelfm 11699  fmfnfmlem2 11701  fmfnfmlem4 11703  fmfnfm 11704  sfcls 11716  filclus 11717  isfclus 11718  fcluscf 11724  flimfcls 11725  flimfnfcls 11727  fcluscomp 11733  tailf 11756  istail 11757  tailmap 11759  tailuni 11761  filnetlem1 11763  filnetlem2 11764  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  filnet 11768  isgalem 11771  ssga 11777  gapm 11784  morex 11804  oprabopabf 11807  f1elima 11818  dif1en 11833  findcard 11836  fimaxg 11838  fipreima 11848  inficl 11849  fzsn 11865  fzm1 11867  absz 11868  sdc 11877  fsumltisum 11887  fsumleisum 11890  fsumlt1 11894  trirn 11897  subspcld2 11902  neificl 11904  metsstop 11909  mettrifi 11912  cncfres 11956  tlmbr 11965  uptx 11978  txcn 11979  txsubsp 11983  totbndbnd 12000  ismtyhmeolem 12006  heiborlem1 12011  heiborlem7 12017  heiborlem10 12020  heiborlem11 12021  heiborlem15 12025  heiborlem18 12028  heiborlem28 12038  heiborlem29 12039  heiborlem30 12040  heiborlem35 12045  heiborlem41 12051  heiborlem42 12052  bfplem3 12056  bfplem8 12061  bfp 12065  reheibor 12081  isphtpc 12101

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-cleq 1511  df-clel 1514

Copyright terms: Public domain