Theorem eleq1 1149

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		cleq2 1110	. . . 4 |- (A = B -> (x = A <-> x = B))
2	1	anbi1d 469	. . 3 |- (A = B -> ((x = A /\ x e. C) <-> (x = B /\ x e. C)))
3	2	biexdv 936	. 2 |- (A = B -> (E.x(x = A /\ x e. C) <-> E.x(x = B /\ x e. C)))
4		df-clel 1099	. 2 |- (A e. C <-> E.x(x = A /\ x e. C))
5		df-clel 1099	. 2 |- (B e. C <-> E.x(x = B /\ x e. C))
6	3, 4, 5	3bitr4g 428	1 |- (A = B -> (A e. C <-> B e. C))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  E.wex 678   = wceq 1091   e. wcel 1092

This theorem is referenced by:  eleq12 1151  eleq1i 1152  eleq1d 1155  eleq1a 1158  cleqf 1167  clneq 1168  hblem 1170  neleq1 1199  rgen2 1248  ralcom2 1314  cbvralf 1330  cbvrex 1332  cbvreuv 1335  reu2 1338  clel2 1374  vtoclga 1387  rcla4v 1402  rcla4ev 1403  eqvinc 1407  ceqsrexv 1413  elabf 1414  elabgf 1416  elrabf 1421  cbvrab 1425  moeq3 1432  mo2icl 1434  ru 1437  dfsbcq 1442  sbc2or 1454  sbcel1 1466  zfaus 1480  eldif 1496  dfss2f 1499  reuhyp 1581  elun 1601  elin 1635  ssex 1700  noel 1711  abn0 1715  elimel 1793  keepel 1796  elpw 1801  elpwg 1802  elsnc2g 1831  disjsn 1836  snssg 1850  sssn 1852  snex 1859  prex 1892  eluni 1922  elunii 1924  eluniab 1926  reuuni2 1956  unipw 1960  elint 1971  elintg 1973  elinti 1974  elintab 1976  intss1 1979  eliun 1998  eliin 1999  ssiun2s 2020  trel 2048  trss 2050  opabss 2100  elopab 2110  epelc 2123  so 2152  supmo 2156  efrirr 2180  tz7.2 2183  nordeq 2218  ordelord 2221  tz7.7 2224  tfis 2245  onint0 2262  oneqmin 2273  onminex 2275  nsuceq0 2306  ordunisuc 2339  onuninsuc 2356  onun 2358  limsuc 2361  limsssuc 2362  nlimsuc 2363  orduninsuc 2365  ordzsl 2366  onzsl 2367  elom 2375  elomg 2376  nnsuc 2389  peano5 2394  findes 2400  tfindes 2404  opelxp 2452  opelxpg 2454  ralxp 2456  opbrop 2472  cbvop 2473  onxpdisj 2476  relss 2480  eldmg 2529  elreldm 2554  imai 2613  elxp4 2640  elxp5 2641  fneu 2728  fcoi2 2766  tz6.12i 2847  ndmfv 2848  fnopabfv 2858  fvelima 2859  fvopab3 2868  fvopab3ig 2869  fvopabn 2873  fvopab2 2878  fvelrn 2883  chfnrn 2885  fvrn 2888  ffnfv 2892  abrexex 2912  tfrlem10 2958  tz7.48lem 2993  tz7.48-1 2994  tz7.49 2997  eloprabg 3035  oprabval 3047  oprabvalig 3048  oprabval4g 3053  oprssdm 3056  caoprmo 3084  oalimcl 3162  oaass 3163  nnaordex 3191  nnawordex 3192  ecelqsi 3229  ecelqsdm 3235  brecop 3242  eceqopreq 3249  th3qlem1 3250  dom2d 3307  mapsnen 3334  xpsnen 3339  pw2en 3348  xpmapenlem5 3395  limensuc 3402  php2 3410  pssnn 3428  ssnn 3429  unblem1 3431  unblem2 3432  unfilem1 3438  eirrv 3449  eirr 3450  sucprcreg 3451  en2lp 3453  inf0 3457  inf3lem6 3469  omelon 3476  setind 3492  tz9.12lem1 3503  tz9.12lem3 3505  tz9.13 3507  tz9.13g 3508  rankval 3512  rankvalg 3513  rankr1 3518  rankr1g 3519  r1pw 3529  r1pwcl 3530  rankonid 3538  rankr1id 3539  scottex 3541  scott0 3542  aceq1 3552  aceq2 3554  aceq3lem 3555  aceq3 3556  aceq5lem1 3558  aceq5lem2 3559  aceq5lem3 3560  aceq5 3563  aceq6a 3564  aceq6b 3565  ac6lem 3575  kmlem2 3581  kmlem4 3583  kmlem14 3593  kmlem15 3594  zornlem4 3606  zornlem5 3607  zorn 3611  oncard 3636  iscard 3659  iscard2 3660  carduni 3664  alephnbtwn 3674  alephle 3689  cardaleph 3690  iscard3 3693  alephsson 3699  cfsuc 3709  axpowndlem3 3745  ltpiord 3809  mulcanpi 3821  addnidpi 3822  indpi 3828  ltexpq 3874  ltexpq2 3875  nsmallpq 3877  ltbtwnpq 3878  prcdpq 3891  prub 3892  prnmax 3893  genpv 3896  genpprecl 3898  genpnmax 3904  distrlem5pr 3925  ltprord 3928  prlem934a 3931  prlem934 3933  ltaddpr2 3935  ltexprlem4 3939  ltexprlem6 3941  ltexprlem7 3942  ltexpri 3943  addcanpr 3946  prlem936 3949  reclem1pr 3950  recexpr 3954  suppr 3957  negexsr 4005  recexsrlem 4006  recexsr 4010  suppsrlem 4015  suppsr 4016  suppsr2 4017  suppsr3 4018  supsrlem2 4020  supsrlem5 4023  supsrlem6 4024  supsr 4025  ltresr 4052  suprelem 4053  supre 4054  axnegex 4078  axrecex 4079  axrnegex 4080  axrrecex 4081  axcnre 4087  mulcant2 4209  dividt 4256  recrect 4260  peano2nn 4433  nnind 4434  nnne0t 4444  sup2 4510  nnunb 4520  elz 4565  elnn0z 4574  nn0subt 4587  elnn0nn 4593  uzind 4603  nnwof 4609  elq 4629  qret 4631  om2uzran 4655  sqr0 4730  sqrlem20 4750  sqr2irrlem1 4777  rere 4810  negre 4825  cjret 4829  clim 4877  clim2 4881  ruclem12 4896  hiidrclt 5053  normlem7t 5072  hlim 5108  hlim2 5112  closedsub 5128  chlim 5139  hlimcau 5142  ch2 5149  ocin 5177  chocuni 5179  omlsilem 5249  omlsi 5250  dfch2 5254  pjch 5269  pjoc1t 5270  pjoc2t 5274  shslej 5339  shsidm 5358  shmods 5363  shjshsel 5413  spanun 5450  h1de2b 5459  h1de2ctlem 5460  h1de2ct 5461  elspansn2t 5472  spansnsst 5476  spanunsn 5482  cmbrt 5494  osumlem1 5530  osumlem7 5536  spansncv 5542  5oalem1 5544  3oalem1 5552  3oalem2 5553  pjch1t 5560  pjcht 5582  pjrn 5587  pjclem4a 5652  pj3lem1 5658  pjnelt 5667  strlem1 5691  cvbrt 5714  mdbr 5726  atom1d 5750  atcvat2t 5773  sumdmdi 5785  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099

metamath.org