Theorem eleq1 1531

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 1481	. . . 4 |- (A = B -> (x = A <-> x = B))
2	1	anbi1d 616	. . 3 |- (A = B -> ((x = A /\ x e. C) <-> (x = B /\ x e. C)))
3	2	exbidv 1277	. 2 |- (A = B -> (E.x(x = A /\ x e. C) <-> E.x(x = B /\ x e. C)))
4		df-clel 1470	. 2 |- (A e. C <-> E.x(x = A /\ x e. C))
5		df-clel 1470	. 2 |- (B e. C <-> E.x(x = B /\ x e. C))
6	3, 4, 5	3bitr4g 554	1 |- (A = B -> (A e. C <-> B e. C))

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

This theorem is referenced by:  eleq12 1533  eleq1i 1534  eleq1d 1537  eleq1a 1540  cleqf 1557  nelneq 1558  hblem 1561  neleq1 1639  rgen2a 1696  ralcom2 1773  cbvralf 1793  cbvrex 1795  cbvreuv 1798  vtoclgaf 1847  rcla4 1867  rcla4e 1868  eqvinc 1879  ceqsrexv 1885  clel2 1887  elabgt 1891  elabf 1892  elabgf 1894  elrabf 1900  cbvrab 1906  abidhb 1908  moeq3 1917  mo2icl 1919  reu2 1926  reu3 1927  rmo4 1929  reu8 1932  ru 1934  dfsbcq 1939  sbc2or 1954  sbcel1gv 1976  hbsbc1gd 1979  hbsbcgd 1980  sbcralt 1986  sbcel12g 2007  sbceqdig 2008  csbiegft 2025  eldif 2053  dfss2f 2056  uniiunlem 2128  elun 2169  elin 2203  noel 2280  abn0 2286  disjne 2311  ifel 2375  ifcl 2376  elimel 2390  keepel 2395  elpw 2400  elpwg 2401  elpr2 2421  elsnc2g 2432  disjsn 2437  rabsn 2441  snssg 2459  prssg 2468  sssn 2469  eluni 2501  elunii 2503  eluniab 2508  elint 2534  elintg 2536  elinti 2537  elintab 2539  elintrabg 2541  intss1 2543  ssintab 2545  intab 2555  eliun 2565  eliin 2566  ssiun2s 2589  iunid 2598  opabss 2663  trel 2682  trss 2684  ssex 2714  intnex 2725  snex 2745  unipw 2751  elopab 2806  opelopab2 2814  epelc 2828  so 2859  reuuni2f 2878  rabxfr 2897  reuhyp 2900  reuunixfr 2901  elpwunsn 2907  efrirr 2923  tz7.2 2926  nordeq 2962  ordelord 2965  tz7.7 2968  onint0 3002  oneqmin 3013  onminex 3015  nsuceq0 3048  ordunisuc 3084  onsucuni2 3086  onuninsuc 3103  onun 3105  nlimsucg 3107  orduninsuc 3109  ordzsl 3111  onzsl 3112  limsssuc 3116  tfis 3122  elom 3129  elomg 3130  nnsuc 3143  peano5 3148  findes 3155  tfindes 3159  opelxp 3209  opelxpg 3211  ralxp 3213  opbrop 3233  onxpdisj 3236  ssrel 3242  ideqg 3271  opelxpex2 3274  eldm2g 3304  breldmg 3311  elreldm 3333  resiexg 3388  imai 3409  elimasng 3419  elxp4 3445  elxp5 3446  xpnz 3458  xpexr 3471  unielrel 3506  relcnvexb 3513  fneu 3584  fcoi2 3637  tz6.12i 3732  ndmfv 3736  fnopabfv 3749  fvelrnb 3751  funimass4 3754  fvelima 3755  fvelimab 3756  ssimaex 3759  fvopab3 3768  fvopab3ig 3769  fvopab4gf 3772  fvopabn 3777  fvopab2 3782  chfnrn 3793  fvelrn 3803  ffnfv 3819  abrexex 3851  elunirnALT 3860  tz7.48lem 3946  tz7.48-1 3947  tz7.49 3950  eloprabg 3998  resoprab 4000  oprabval 4014  oprabvalig 4015  oprabval2gf 4017  oprabval4g 4022  oprabval6g 4023  oprvalelrn 4030  oprssdm 4033  caoprmo 4062  2ndconst 4087  eqop 4094  unielxp 4097  elopabi 4107  eloprabi 4108  oalimcl 4184  oaass 4185  omlimcl 4199  odi 4200  nnaordex 4239  nnawordex 4240  ecelqsi 4282  ecelqsdm 4289  brecop 4296  eceqopreq 4303  th3qlem1 4304  dom2d 4391  mapsnen 4416  xpsnen 4421  pw2en 4432  xpmapenlem5 4486  limensuc 4493  php2 4500  ssnn 4520  unblem1 4523  unblem2 4524  unfilem1 4530  abfii2 4542  supmo 4556  elirrv 4578  elirr 4579  sucprcreg 4580  en2lp 4582  inf0 4586  inf3lem6 4598  omelon 4609  noinfep 4620  setind 4628  tz9.12lem1 4639  tz9.12lem3 4641  tz9.13 4643  tz9.13g 4644  rankval 4648  rankvalg 4649  rankr1 4654  rankr1g 4655  r1pw 4666  r1pwcl 4667  rankonid 4675  rankr1id 4677  rankuni 4678  rankc2 4686  rankxpsuc 4695  scottex 4696  scott0 4697  aceq1 4709  aceq2 4711  aceq3lem 4712  aceq3 4713  aceq5lem1 4715  aceq5lem2 4716  aceq5lem3 4717  aceq5 4720  aceq6a 4721  aceq6b 4722  ac6lem 4734  ac6s4 4741  kmlem2 4746  kmlem4 4748  kmlem14 4758  kmlem15 4759  zorn2lem4 4771  zorn2lem5 4772  zorn2 4776  unidom 4788  oncard 4809  iscard 4833  iscard2 4834  carduni 4838  alephnbtwn 4848  alephle 4864  cardaleph 4865  iscard3 4868  alephsson 4874  alephval3 4883  cfsuc 4895  axpowndlem3 4931  ltpiord 4995  mulcanpi 5007  addnidpi 5008  indpi 5014  ltexpq 5060  ltexpq2 5061  nsmallpq 5063  ltbtwnpq 5064  prcdpq 5077  prub 5078  prnmax 5079  genpv 5082  genpprecl 5084  genpnmax 5090  distrlem5pr 5111  ltprord 5114  prlem934a 5117  prlem934 5119  ltaddpr2 5121  ltexprlem4 5125  ltexprlem6 5127  ltexprlem7 5128  ltexpri 5129  addcanpr 5132  prlem936 5135  reclem1pr 5136  recexpr 5140  supexpr 5143  negexsr 5191  recexsrlem 5192  recexsr 5196  suppsrlem 5201  suppsr 5202  suppsr2 5203  suppsr3 5204  supsrlem2 5206  supsrlem5 5209  supsrlem6 5210  supsr 5211  ltresr 5238  suprelem 5239  supre 5240  axrnegex 5263  axrrecex 5264  axcnre 5266  0cnALT 5330  1re 5415  ltxrltt 5480  ssxr 5521  mulcant 5669  div11t 5729  recrect 5740  nnne0t 5905  sup2 6006  infm3 6009  infmsup 6023  nnunb 6025  elz 6092  elnn0z 6102  nn0subt 6116  elnn0nn 6126  peano5uzt 6160  uzindOLD 6164  elq 6203  qret 6205  om2uzran 6245  snunioolem 6355  uzind4s 6392  uzind4s2 6393  nnwof 6399  elfzp1 6450  fz1sbct 6457  limsupclt 6470  sqr0 6610  sqrlem20 6630  sqr2irrlem1 6662  rereb 6723  negreb 6738  cjrebt 6743  nn0absclt 6824  bcpasc2t 6914  clim 6923  climshft 7049  climcmplem 7081  cvgcmp3cetlem1 7132  reccnv 7161  infcvgaux1 7162  infcvgaux2 7163  expcnvlem5 7174  expcnv 7176  geolim 7180  geolim1 7182  mulc1cncf 7222  efseq1ex 7256  absef01tlub 7337  eflegeot 7364  efm1legeot 7366  efcnlem4 7370  reeff1olem2 7373  reeff1olem2OLD 7375  acdc3 7437  acdc2 7440  acdc5 7443  acdc 7445  ruclem12 7472  eltopsp 7554  tpsex 7555  istps 7556  basis2t 7565  tg2t 7571  eltg3t 7576  subbas2 7595  iscld3 7645  isopn3 7647  islp2 7697  cnpval 7709  cnpco 7719  cncnplem2 7725  cnconst 7730  hausnei 7734  sncld 7737  blin 7804  opni 7816  opnin 7821  lmbr 7880  metelcls 7916  fsumcnlem 7939  bcthlem15 7963  bcth 7982  isgrp2i 8026  isring 8093  ringi 8094  vci 8119  isvclem 8148  nvvcop 8165  nmosetre 8372  blocni 8409  blocn 8411  isph 8425  siilem2 8456  spwmo 8598  circgrp 8679  effoi 8684  avril1 8723  normlem7tALT 8924  hlim 8995  hlim2 8999  closedsub 9032  chlim 9043  hlimcau 9046  ch2 9053  hhssnv 9073  hhsssh 9078  ocin 9108  chocuni 9111  pjeqt 9180  omlsilem 9182  omlsi 9183  dfch2 9187  pjch 9203  pjoc1t 9205  pjoc2t 9210  shslej 9276  shsidm 9295  shmods 9300  shjshsel 9354  spanun 9405  h1de2b 9415  h1de2bOLD 9416  h1de2ctlem 9417  h1de2ct 9418  elspansn2t 9429  spansnsst 9434  spanunsn 9442  cmbrt 9467  osumlem1 9518  osumlem7 9524  spansncv 9537  5oalem1 9539  3oalem1 9547  3oalem2 9548  pjch1t 9555  pjcht 9579  pjrn 9587  pjnelt 9611  eigret 9701  nmopsetretALT 9730  nmfnsetret 9744  elunop2t 9876  lnophmt 9882  lnopcont 9902  nmbdfnlbt 9917  lnfncont 9929  adjbd1o 9956  adjeq0 9962  bra11 9979  hmopidmcht 10019  hmopidmpjt 10020  pjssdif1 10041  elpjrncht 10056  pjclem4a 10064  pjcmmul2 10068  pj3lem1 10072  strlem1 10115  cvbrt 10147  mdbrt 10159  dmdbrt 10164  atom1d 10217  shatomistic 10225  atcvat2t 10253  irredt 10259  sumdmdi 10278  sumdmdlem 10281  cdjreu 10293  ghomgrplem 10323  cayleythlem 10347  gelsupvalOLD 10354  cbvrexf 10374  uninqs 10378  elo 10381  fiiu 10386  stcat 10389  cmpbva 10396  fiv 10410  fiiu2 10413  mapudiscn 10435  hmph 10447  hmphsyma 10451  hmphre 10453  hmphtr 10454  hmeogrp 10461  homcard 10462  fillsb 10471  filint 10473  filintf 10479  fgsb 10480  cnfilca 10487  iint 10514  trran 10516  trnij 10517  cnvtr 10518  eloi 10539  rdmob 10561  ishomc 10597  ismonb 10616

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-cleq 1467  df-clel 1470

Copyright terms: Public domain