Theorem eleq1 2292

Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem eleq1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2239	. . . 4 |- ( A = B -> ( x = A <-> x = B ) )
2	1	anbi1d 465	. . 3 |- ( A = B -> ( ( x = A /\ x e. C ) <-> ( x = B /\ x e. C ) ) )
3	2	exbidv 1871	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2225	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2225	. 2 |- ( B e. C <-> E. x ( x = B /\ x e. C ) )
6	3, 4, 5	3bitr4g 223	1 |- ( A = B -> ( A e. C <-> B e. C ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1395   E.wex 1538   e. wcel 2200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12  2294  eleq1i  2295  eleq1d  2298  eleq1a  2301  cleqh  2329  nelneq  2330  clelsb1  2334  nfcjust  2360  cleqf  2397  nelne2  2491  neleq1  2499  rgen2a  2584  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvrab  2797  eqvisset  2810  ceqsralt  2827  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  rspct  2900  rspc  2901  rspce  2902  rspc2gv  2919  ceqsrexv  2933  ceqsrexbv  2934  clel2  2936  elabgt  2944  elabgf  2945  elrabi  2956  elrabf  2957  elrab3t  2958  ralab2  2967  rexab2  2969  mo2icl  2982  morex  2987  reu2  2991  reu6  2992  rmo4  2996  reu8  2999  reuind  3008  nelrdva  3010  ru  3027  dfsbcq  3030  dfsbcq2  3031  sbc8g  3036  sbcel1v  3091  rmob  3122  difjust  3198  unjust  3200  injust  3202  eldif  3206  dfss2f  3215  uniiunlem  3313  elun  3345  elin  3387  rabn0m  3519  disjne  3545  r19.3rm  3580  r19.9rmv  3583  raaanlem  3596  raaan  3597  elif  3614  ifmdc  3645  elpwg  3657  elpr2  3688  elsn2g  3699  rabsn  3733  tpid3g  3782  snssb  3801  snssgOLD  3804  difsn  3805  sssnm  3832  opeq1  3857  opeq2  3858  eluni  3891  elunii  3893  eluniab  3900  elint  3929  elintg  3931  elintab  3934  elintrabg  3936  intss1  3938  eliun  3969  eliin  3970  dfiunv2  4001  opabss  4148  cbvmpt  4179  trel  4189  trss  4191  ssex  4221  intnexr  4235  intexabim  4236  exmidel  4289  euabex  4311  elopab  4346  opelopab2a  4353  frirrg  4441  tz7.2  4445  ordelord  4472  onm  4492  ralxfr2d  4555  rexxfr2d  4556  rabxfrd  4560  reuhypd  4562  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmid  4622  ordsucunielexmid  4623  regexmidlem1  4625  elirr  4633  nordeq  4636  sucprcreg  4641  en2lp  4646  ordsoexmid  4654  ordsuc  4655  onsucuni2  4656  tfis  4675  peano2  4687  findes  4695  limom  4706  opelxp  4749  opeliunxp  4774  opbrop  4798  ssrel  4807  ssrel2  4809  ssrelrel  4819  relopabi  4847  eliunxp  4861  opeliunxp2  4862  ideqg  4873  reldmm  4942  dmmrnm  4943  dmxpm  4944  elreldm  4950  elrnmptg  4976  elres  5041  resiexg  5050  dfres2  5057  imai  5084  elimasng  5096  issref  5111  xpmlem  5149  xpm  5150  elxp4  5216  elxp5  5217  unielrel  5256  relcnvexb  5268  dmfex  5517  funfveu  5642  funimass4  5686  fvelimab  5692  ssimaex  5697  fvopab3g  5709  fvopab3ig  5710  fvmptssdm  5721  chfnrn  5748  fvelrn  5768  fmpt  5787  ffnfv  5795  fmptco  5803  elunirn  5896  f1elima  5903  cbvriota  5972  acexmidlemab  6001  acexmidlemcase  6002  cbvmpox  6088  eloprabga  6097  resoprab  6106  elrnmpo  6124  ov  6130  ovig  6132  ov6g  6149  ovg  6150  ovelrn  6160  caovimo  6205  fo1stresm  6313  fo2ndresm  6314  elxp6  6321  unielxp  6326  eqop2  6330  dfoprab4  6344  dfoprab4f  6345  fmpox  6352  1stconst  6373  2ndconst  6374  f1o2ndf1  6380  xporderlem  6383  f1od2  6387  disjxp1  6388  opeliunxp2f  6390  dftpos3  6414  dftpos4  6415  tpostpos  6416  smoel  6452  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfrcl  6516  frecabcl  6551  frecsuc  6559  nntri3or  6647  nntri3  6651  nndcel  6654  riinerm  6763  th3qlem1  6792  mapsncnv  6850  elixpsn  6890  dom2lem  6931  fiprc  6976  xpsnen  6988  phplem3g  7025  phpelm  7036  ssfiexmid  7046  domfiexmid  7048  elssdc  7075  inffiexmid  7079  undifdcss  7096  opabfi  7111  snon0  7113  f1dmvrnfibi  7122  f1vrnfibi  7123  ordiso2  7213  ctssdclemn0  7288  ctssdc  7291  enumct  7293  nnnninf  7304  nnnninfeq  7306  nninfisollemne  7309  nninfisol  7311  finomni  7318  exmidlpo  7321  pr2cv1  7379  acneq  7395  finacn  7397  acfun  7400  exmidontriimlem3  7416  exmidontriimlem4  7417  pw1ne1  7425  onntri35  7433  exmidapne  7457  ccfunen  7461  cc2lem  7463  elni2  7512  recexnq  7588  recmulnqg  7589  enq0enq  7629  enq0sym  7630  enq0ref  7631  enq0tr  7632  enq0breq  7634  nqnq0pi  7636  nqnq0  7639  prop  7673  prcdnql  7682  prcunqu  7683  prubl  7684  prltlu  7685  prnmaxl  7686  prnminu  7687  prdisj  7690  prarloc  7701  genipv  7707  genpelvl  7710  genpelvu  7711  genprndl  7719  genprndu  7720  distrlem5prl  7784  distrlem5pru  7785  ltexprlemm  7798  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  aptiprleml  7837  aptiprlemu  7838  archpr  7841  cauappcvgprlemm  7843  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  caucvgprlemm  7866  caucvgprlemladdfu  7875  caucvgprprlemmu  7893  elreal2  8028  ltresr  8037  axcnre  8079  axpre-suploclemres  8099  0re  8157  renepnf  8205  renemnf  8206  ltxrlt  8223  eqlei2  8252  0cnALT  8347  sup3exmid  9115  nn1suc  9140  nnne0  9149  xnn0xr  9448  nn0nepnf  9451  elz  9459  elnn0z  9470  elz2  9529  uzind4s  9797  elnn1uz2  9814  qre  9832  elpqb  9857  xnn0lenn0nn0  10073  xsubge0  10089  xposdif  10090  xleaddadd  10095  fzsn  10274  fz1sbc  10304  elfzp12  10307  fzm1  10308  fz01or  10319  fvinim0ffz  10459  suprzubdc  10468  zsupssdc  10470  xqltnle  10499  flqidz  10518  ceilqidz  10550  modqmuladdnn0  10602  frec2uzrand  10639  frecuzrdgtcl  10646  fzfig  10664  seq3fveq2  10709  seqfveq2g  10711  seq3shft2  10715  seqshft2g  10716  monoord  10719  seq3split  10722  seqsplitg  10723  iseqf1olemqval  10734  seq3id2  10760  seqhomog  10764  1exp  10802  bcval  10983  hashennn  11014  zfz1isolem1  11075  zfz1iso  11076  seq3coll  11077  iswrdiz  11091  0wrd0  11110  lswlgt0cl  11137  ccatval1  11145  ccatval2  11146  ccatalpha  11161  ccatrcl1  11162  wrdl1s1  11178  ccats1val2  11187  wrd2ind  11271  pfxccatin12lem3  11280  pfxccatid  11289  reuccatpfxs1lem  11294  shftlem  11343  shftfibg  11347  shftfib  11350  shftfn  11351  2shfti  11358  rexuz3  11517  sqrt0rlem  11530  cau3  11642  negfi  11755  sumdc  11885  sumrbdclem  11904  summodclem2a  11908  fisumss  11919  prodrbdclem  12098  prodmodclem2a  12103  fprodssdc  12117  fprodsplit1f  12161  ef0lem  12187  odd2np1  12400  even2n  12401  oddnn02np1  12407  oddge22np1  12408  evennn02n  12409  evennn2n  12410  nn0enne  12429  divalgmod  12454  uzwodc  12574  lcmgcdlem  12615  cncongr1  12641  1nprm  12652  isprm2  12655  dvdsnprmd  12663  prmdc  12668  exprmfct  12676  nprmdvds1  12678  coprm  12682  prmdiveq  12774  prm23lt5  12802  pcpre1  12831  pc2dvds  12869  pcz  12871  pcmpt  12882  qexpz  12891  4sqlem2  12928  4sqlem19  12948  ennnfonelemhom  13002  ctiunctlemudc  13024  ssnnctlemct  13033  nninfdclemcl  13035  imasaddfnlemg  13363  ismgmid  13426  isgrpid2  13589  mhmlem  13667  eqgval  13776  dvdsrcl2  14079  nzrunit  14168  lringuplu  14176  dvdsrzring  14583  znrrg  14640  mplsubgfilemm  14678  fiinopn  14694  istopon  14703  basis2  14738  eltg3  14747  tg2  14750  tgidm  14764  bastop  14765  bastop2  14774  topnex  14776  isopn3  14815  tgrest  14859  cnpval  14888  lmbr  14903  cnconst  14924  txbas  14948  uptx  14964  txdis1cn  14968  cnmpt12  14977  cnmpt22  14984  hmeocnvb  15008  xblm  15107  isxms2  15142  mopni  15172  blssioo  15243  dedekindeulemuub  15307  dedekindeulemeu  15312  dedekindicclemuub  15316  dedekindicclemeu  15321  ivthinclemlm  15324  ivthinclemum  15325  ivthreinc  15335  lgsfvalg  15700  lgsval2lem  15705  lgsdir2lem2  15724  gausslemma2dlem1a  15753  gausslemma2dlem4  15759  gausslemma2dlem6  15762  2lgslem1b  15784  2lgs  15799  2lgsoddprmlem2  15801  2lgsoddprmlem3  15806  2sqlem2  15810  2sqlem6  15815  2sqlem7  15816  2sqlem10  15820  vtxvalg  15833  iedgvalg  15834  umgredg  15959  upgrpredgv  15960  usgredg2vlem2  16037  ushgredgedg  16040  ushgredgedgloop  16042  vtxdgfifival  16051  iswlk  16069  upgrwlkvtxedg  16110  isclwwlknx  16158  clwwlkn1loopb  16162  elabgf0  16224  bj-rspgt  16233  cbvrald  16235  decidi  16242  sumdc2  16246  bdssex  16348  bj-inex  16353  bj-intnexr  16355  bj-unexg  16367  bj-d0clsepcl  16371  bj-nnelirr  16399  bj-nn0suc  16410  bj-inf2vnlem1  16416  bj-inf2vnlem2  16417  bj-inf2vnlem3  16418  bj-inf2vnlem4  16419  bj-nn0sucALT  16424  bj-findis  16425  3dom  16439  trilpolemcl  16493