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  5515  funfveu  5640  funimass4  5684  fvelimab  5690  ssimaex  5695  fvopab3g  5707  fvopab3ig  5708  fvmptssdm  5719  chfnrn  5746  fvelrn  5766  fmpt  5785  ffnfv  5793  fmptco  5801  elunirn  5890  f1elima  5897  cbvriota  5966  acexmidlemab  5995  acexmidlemcase  5996  cbvmpox  6082  eloprabga  6091  resoprab  6100  elrnmpo  6118  ov  6124  ovig  6126  ov6g  6143  ovg  6144  ovelrn  6154  caovimo  6199  fo1stresm  6307  fo2ndresm  6308  elxp6  6315  unielxp  6320  eqop2  6324  dfoprab4  6338  dfoprab4f  6339  fmpox  6346  1stconst  6367  2ndconst  6368  f1o2ndf1  6374  xporderlem  6377  f1od2  6381  disjxp1  6382  opeliunxp2f  6384  dftpos3  6408  dftpos4  6409  tpostpos  6410  smoel  6446  tfr1onlemaccex  6494  tfrcllemaccex  6507  tfrcl  6510  frecabcl  6545  frecsuc  6553  nntri3or  6639  nntri3  6643  nndcel  6646  riinerm  6755  th3qlem1  6784  mapsncnv  6842  elixpsn  6882  dom2lem  6923  fiprc  6968  xpsnen  6980  phplem3g  7017  phpelm  7028  ssfiexmid  7038  domfiexmid  7040  inffiexmid  7068  undifdcss  7085  opabfi  7100  snon0  7102  f1dmvrnfibi  7111  f1vrnfibi  7112  ordiso2  7202  ctssdclemn0  7277  ctssdc  7280  enumct  7282  nnnninf  7293  nnnninfeq  7295  nninfisollemne  7298  nninfisol  7300  finomni  7307  exmidlpo  7310  pr2cv1  7368  acneq  7384  finacn  7386  acfun  7389  exmidontriimlem3  7405  exmidontriimlem4  7406  pw1ne1  7414  onntri35  7422  exmidapne  7446  ccfunen  7450  cc2lem  7452  elni2  7501  recexnq  7577  recmulnqg  7578  enq0enq  7618  enq0sym  7619  enq0ref  7620  enq0tr  7621  enq0breq  7623  nqnq0pi  7625  nqnq0  7628  prop  7662  prcdnql  7671  prcunqu  7672  prubl  7673  prltlu  7674  prnmaxl  7675  prnminu  7676  prdisj  7679  prarloc  7690  genipv  7696  genpelvl  7699  genpelvu  7700  genprndl  7708  genprndu  7709  distrlem5prl  7773  distrlem5pru  7774  ltexprlemm  7787  ltexprlemdisj  7793  ltexprlemloc  7794  ltexprlemrl  7797  ltexprlemru  7799  aptiprleml  7826  aptiprlemu  7827  archpr  7830  cauappcvgprlemm  7832  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  caucvgprlemm  7855  caucvgprlemladdfu  7864  caucvgprprlemmu  7882  elreal2  8017  ltresr  8026  axcnre  8068  axpre-suploclemres  8088  0re  8146  renepnf  8194  renemnf  8195  ltxrlt  8212  eqlei2  8241  0cnALT  8336  sup3exmid  9104  nn1suc  9129  nnne0  9138  xnn0xr  9437  nn0nepnf  9440  elz  9448  elnn0z  9459  elz2  9518  uzind4s  9785  elnn1uz2  9802  qre  9820  elpqb  9845  xnn0lenn0nn0  10061  xsubge0  10077  xposdif  10078  xleaddadd  10083  fzsn  10262  fz1sbc  10292  elfzp12  10295  fzm1  10296  fz01or  10307  fvinim0ffz  10447  suprzubdc  10456  zsupssdc  10458  xqltnle  10487  flqidz  10506  ceilqidz  10538  modqmuladdnn0  10590  frec2uzrand  10627  frecuzrdgtcl  10634  fzfig  10652  seq3fveq2  10697  seqfveq2g  10699  seq3shft2  10703  seqshft2g  10704  monoord  10707  seq3split  10710  seqsplitg  10711  iseqf1olemqval  10722  seq3id2  10748  seqhomog  10752  1exp  10790  bcval  10971  hashennn  11002  zfz1isolem1  11062  zfz1iso  11063  seq3coll  11064  iswrdiz  11078  0wrd0  11097  lswlgt0cl  11124  ccatval1  11132  ccatval2  11133  wrdl1s1  11163  ccats1val2  11171  wrd2ind  11255  pfxccatin12lem3  11264  pfxccatid  11273  reuccatpfxs1lem  11278  shftlem  11327  shftfibg  11331  shftfib  11334  shftfn  11335  2shfti  11342  rexuz3  11501  sqrt0rlem  11514  cau3  11626  negfi  11739  sumdc  11869  sumrbdclem  11888  summodclem2a  11892  fisumss  11903  prodrbdclem  12082  prodmodclem2a  12087  fprodssdc  12101  fprodsplit1f  12145  ef0lem  12171  odd2np1  12384  even2n  12385  oddnn02np1  12391  oddge22np1  12392  evennn02n  12393  evennn2n  12394  nn0enne  12413  divalgmod  12438  uzwodc  12558  lcmgcdlem  12599  cncongr1  12625  1nprm  12636  isprm2  12639  dvdsnprmd  12647  prmdc  12652  exprmfct  12660  nprmdvds1  12662  coprm  12666  prmdiveq  12758  prm23lt5  12786  pcpre1  12815  pc2dvds  12853  pcz  12855  pcmpt  12866  qexpz  12875  4sqlem2  12912  4sqlem19  12932  ennnfonelemhom  12986  ctiunctlemudc  13008  ssnnctlemct  13017  nninfdclemcl  13019  imasaddfnlemg  13347  ismgmid  13410  isgrpid2  13573  mhmlem  13651  eqgval  13760  dvdsrcl2  14063  nzrunit  14152  lringuplu  14160  dvdsrzring  14567  znrrg  14624  mplsubgfilemm  14662  fiinopn  14678  istopon  14687  basis2  14722  eltg3  14731  tg2  14734  tgidm  14748  bastop  14749  bastop2  14758  topnex  14760  isopn3  14799  tgrest  14843  cnpval  14872  lmbr  14887  cnconst  14908  txbas  14932  uptx  14948  txdis1cn  14952  cnmpt12  14961  cnmpt22  14968  hmeocnvb  14992  xblm  15091  isxms2  15126  mopni  15156  blssioo  15227  dedekindeulemuub  15291  dedekindeulemeu  15296  dedekindicclemuub  15300  dedekindicclemeu  15305  ivthinclemlm  15308  ivthinclemum  15309  ivthreinc  15319  lgsfvalg  15684  lgsval2lem  15689  lgsdir2lem2  15708  gausslemma2dlem1a  15737  gausslemma2dlem4  15743  gausslemma2dlem6  15746  2lgslem1b  15768  2lgs  15783  2lgsoddprmlem2  15785  2lgsoddprmlem3  15790  2sqlem2  15794  2sqlem6  15799  2sqlem7  15800  2sqlem10  15804  vtxvalg  15817  iedgvalg  15818  umgredg  15943  upgrpredgv  15944  usgredg2vlem2  16021  ushgredgedg  16024  ushgredgedgloop  16026  iswlk  16036  upgrwlkvtxedg  16075  elabgf0  16141  bj-rspgt  16150  cbvrald  16152  decidi  16159  sumdc2  16163  bdssex  16265  bj-inex  16270  bj-intnexr  16272  bj-unexg  16284  bj-d0clsepcl  16288  bj-nnelirr  16316  bj-nn0suc  16327  bj-inf2vnlem1  16333  bj-inf2vnlem2  16334  bj-inf2vnlem3  16335  bj-inf2vnlem4  16336  bj-nn0sucALT  16341  bj-findis  16342  trilpolemcl  16405