Theorem eleq1 2297

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 2244	. . . 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 1874	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2230	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2230	. 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 1398   E.wex 1541   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eleq12  2299  eleq1i  2300  eleq1d  2303  eleq1a  2306  cleqh  2334  nelneq  2335  clelsb1  2339  nfcjust  2374  cleqf  2411  nelne2  2505  neleq1  2513  rgen2a  2598  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvrab  2813  eqvisset  2826  ceqsralt  2843  vtoclgaf  2882  vtocl2gaf  2884  vtocl3gaf  2886  rspct  2916  rspc  2917  rspce  2918  rspc2gv  2935  ceqsrexv  2949  ceqsrexbv  2950  clel2  2952  elabgt  2960  elabgf  2961  elrabi  2972  elrabf  2973  elrab3t  2974  ralab2  2983  rexab2  2985  mo2icl  2998  morex  3003  reu2  3007  reu6  3008  rmo4  3012  reu8  3015  reuind  3024  nelrdva  3026  ru  3043  dfsbcq  3046  dfsbcq2  3047  sbc8g  3052  sbcel1v  3107  rmob  3138  difjust  3214  unjust  3216  injust  3218  eldif  3222  dfss2f  3231  uniiunlem  3330  elun  3362  elin  3404  rabn0m  3538  disjne  3564  r19.3rm  3600  r19.9rmv  3603  raaanlem  3616  raaan  3617  elif  3636  ifmdc  3667  elpwg  3679  elpr2  3713  elsn2g  3724  rabsn  3758  tpid3g  3809  snssb  3829  snssgOLD  3832  difsn  3833  sssnm  3860  opeq1  3885  opeq2  3886  eluni  3919  elunii  3921  eluniab  3928  elint  3957  elintg  3959  elintab  3962  elintrabg  3964  intss1  3966  eliun  3997  eliin  3998  dfiunv2  4029  opabss  4176  cbvmpt  4207  trel  4217  trss  4219  ssex  4249  intnexr  4265  intexabim  4266  exmidel  4320  euabex  4343  elopab  4378  opelopab2a  4385  frirrg  4473  tz7.2  4477  ordelord  4504  onm  4524  ralxfr2d  4587  rexxfr2d  4588  rabxfrd  4592  reuhypd  4594  ordtriexmid  4645  ontriexmidim  4646  ordtri2orexmid  4647  ontr2exmid  4649  onsucsssucexmid  4651  onsucelsucexmid  4654  ordsucunielexmid  4655  regexmidlem1  4657  elirr  4665  nordeq  4668  sucprcreg  4673  en2lp  4678  ordsoexmid  4686  ordsuc  4687  onsucuni2  4688  tfis  4707  peano2  4719  findes  4727  limom  4738  opelxp  4781  opeliunxp  4807  opbrop  4831  ssrel  4840  ssrel2  4842  ssrelrel  4852  relopabi  4882  eliunxp  4896  opeliunxp2  4897  ideqg  4908  reldmm  4977  dmmrnm  4978  dmxpm  4979  elreldm  4985  elrnmptg  5011  elres  5076  resiexg  5085  dfres2  5092  imai  5120  elimasng  5132  issref  5147  xpmlem  5185  xpm  5186  elxp4  5252  elxp5  5253  unielrel  5292  relcnvexb  5304  dmfex  5559  funfveu  5685  funimass4  5729  fvelimab  5735  ssimaex  5740  fvopab3g  5752  fvopab3ig  5753  fvmptssdm  5764  chfnrn  5791  fvelrn  5810  fmpt  5829  ffnfv  5837  fmptco  5845  elunirn  5941  f1elima  5948  cbvriota  6017  acexmidlemab  6046  acexmidlemcase  6047  cbvmpox  6133  eloprabga  6142  resoprab  6151  elrnmpo  6169  ov  6175  ovig  6177  ov6g  6194  ovg  6195  ovelrn  6205  caovimo  6250  fo1stresm  6357  fo2ndresm  6358  elxp6  6365  unielxp  6370  eqop2  6374  dfoprab4  6388  dfoprab4f  6389  fmpox  6398  1stconst  6419  2ndconst  6420  f1o2ndf1  6426  xporderlem  6429  f1od2  6433  disjxp1  6434  opeliunxp2f  6471  dftpos3  6495  dftpos4  6496  tpostpos  6497  smoel  6533  tfr1onlemaccex  6581  tfrcllemaccex  6594  tfrcl  6597  frecabcl  6632  frecsuc  6640  nntri3or  6728  nntri3  6732  nndcel  6735  riinerm  6844  th3qlem1  6873  mapsncnv  6932  elixpsn  6972  dom2lem  7013  fiprc  7059  xpsnen  7074  phplem3g  7112  phpelm  7123  ssfiexmid  7133  ssfiexmidt  7135  domfiexmid  7137  elssdc  7164  inffiexmid  7168  undifdcss  7185  opabfi  7202  snon0  7204  f1dmvrnfibi  7213  f1vrnfibi  7214  suppeqfsuppbi  7250  ordiso2  7328  ctssdclemn0  7403  ctssdc  7406  enumct  7408  nnnninf  7419  nnnninfeq  7421  nninfisollemne  7424  nninfisol  7426  finomni  7433  exmidlpo  7436  pr2cv1  7494  acneq  7511  finacn  7513  acfun  7516  exmidontriimlem3  7532  exmidontriimlem4  7533  pw1ne1  7541  onntri35  7549  exmidapne  7576  ccfunen  7580  cc2lem  7582  elni2  7631  recexnq  7707  recmulnqg  7708  enq0enq  7748  enq0sym  7749  enq0ref  7750  enq0tr  7751  enq0breq  7753  nqnq0pi  7755  nqnq0  7758  prop  7792  prcdnql  7801  prcunqu  7802  prubl  7803  prltlu  7804  prnmaxl  7805  prnminu  7806  prdisj  7809  prarloc  7820  genipv  7826  genpelvl  7829  genpelvu  7830  genprndl  7838  genprndu  7839  distrlem5prl  7903  distrlem5pru  7904  ltexprlemm  7917  ltexprlemdisj  7923  ltexprlemloc  7924  ltexprlemrl  7927  ltexprlemru  7929  aptiprleml  7956  aptiprlemu  7957  archpr  7960  cauappcvgprlemm  7962  cauappcvgprlemladdfu  7971  cauappcvgprlemladdfl  7972  caucvgprlemm  7985  caucvgprlemladdfu  7994  caucvgprprlemmu  8012  elreal2  8147  ltresr  8156  axcnre  8198  axpre-suploclemres  8218  0re  8276  renepnf  8323  renemnf  8324  ltxrlt  8341  eqlei2  8370  0cnALT  8465  sup3exmid  9233  nn1suc  9258  nnne0  9267  xnn0xr  9570  nn0nepnf  9573  elz  9581  elnn0z  9592  elz2  9651  uzind4s  9925  elnn1uz2  9942  qre  9960  elpqb  9985  xnn0lenn0nn0  10201  xsubge0  10217  xposdif  10218  xleaddadd  10223  fzsn  10403  fz1sbc  10434  elfzp12  10437  fzm1  10438  fz01or  10449  fvinim0ffz  10591  suprzubdc  10600  zsupssdc  10602  xqltnle  10631  flqidz  10650  ceilqidz  10682  modqmuladdnn0  10734  frec2uzrand  10771  frecuzrdgtcl  10778  fzfig  10796  seq3fveq2  10841  seqfveq2g  10843  seq3shft2  10847  seqshft2g  10848  monoord  10851  seq3split  10854  seqsplitg  10855  iseqf1olemqval  10866  seq3id2  10892  seqhomog  10896  1exp  10934  bcval  11115  hashennn  11147  hashfibc  11211  zfz1isolem1  11216  zfz1iso  11217  seq3coll  11218  iswrdiz  11235  0wrd0  11254  lswlgt0cl  11281  ccatval1  11289  ccatval2  11290  ccatalpha  11305  ccatrcl1  11306  wrdl1s1  11322  ccats1val2  11332  wrd2ind  11419  pfxccatin12lem3  11428  pfxccatid  11437  reuccatpfxs1lem  11442  shftlem  11505  shftfibg  11509  shftfib  11512  shftfn  11513  2shfti  11520  rexuz3  11679  sqrt0rlem  11692  cau3  11804  negfi  11917  sumdc  12047  sumrbdclem  12067  summodclem2a  12071  fisumss  12082  prodrbdclem  12261  prodmodclem2a  12266  fprodssdc  12280  fprodsplit1f  12324  ef0lem  12350  odd2np1  12563  even2n  12564  oddnn02np1  12570  oddge22np1  12571  evennn02n  12572  evennn2n  12573  nn0enne  12592  divalgmod  12617  uzwodc  12737  lcmgcdlem  12778  cncongr1  12804  1nprm  12815  isprm2  12818  dvdsnprmd  12826  prmdc  12831  exprmfct  12839  nprmdvds1  12841  coprm  12845  prmdiveq  12937  prm23lt5  12965  pcpre1  12994  pc2dvds  13032  pcz  13034  pcmpt  13045  qexpz  13054  4sqlem2  13091  4sqlem19  13111  ballotfilem2  13149  ballotfilemfc0  13153  ballotfilemfcc  13154  ennnfonelemhom  13183  ctiunctlemudc  13205  ssnnctlemct  13214  nninfdclemcl  13216  imasaddfnlemg  13544  ismgmid  13607  isgrpid2  13770  mhmlem  13848  eqgval  13957  dvdsrcl2  14261  nzrunit  14350  lringuplu  14358  dvdsrzring  14768  znrrg  14825  mplsubgfilemm  14870  fiinopn  14886  istopon  14895  basis2  14930  eltg3  14939  tg2  14942  tgidm  14956  bastop  14957  bastop2  14966  topnex  14968  isopn3  15007  tgrest  15051  cnpval  15080  lmbr  15095  cnconst  15116  txbas  15140  uptx  15156  txdis1cn  15160  cnmpt12  15169  cnmpt22  15176  hmeocnvb  15200  xblm  15299  isxms2  15334  mopni  15364  blssioo  15435  dedekindeulemuub  15499  dedekindeulemeu  15504  dedekindicclemuub  15508  dedekindicclemeu  15513  ivthinclemlm  15516  ivthinclemum  15517  ivthreinc  15527  pellexlem3  15864  lgsfvalg  15895  lgsval2lem  15900  lgsdir2lem2  15919  gausslemma2dlem1a  15948  gausslemma2dlem4  15954  gausslemma2dlem6  15957  2lgslem1b  15979  2lgs  15994  2lgsoddprmlem2  15996  2lgsoddprmlem3  16001  2sqlem2  16005  2sqlem6  16010  2sqlem7  16011  2sqlem10  16015  vtxvalg  16028  iedgvalg  16029  umgredg  16157  upgrpredgv  16158  usgredg2vlem2  16235  ushgredgedg  16238  ushgredgedgloop  16240  griedg0ssusgr  16263  uhgrspansubgrlem  16288  vtxdgfifival  16303  iswlk  16335  upgrwlkvtxedg  16376  isclwwlknx  16428  clwwlkn1loopb  16432  clwwlknonex2lem1  16449  elabgf0  16566  bj-rspgt  16575  cbvrald  16577  decidi  16584  sumdc2  16588  bdssex  16689  bj-inex  16694  bj-intnexr  16696  bj-unexg  16708  bj-d0clsepcl  16712  bj-nnelirr  16740  bj-nn0suc  16751  bj-inf2vnlem1  16757  bj-inf2vnlem2  16758  bj-inf2vnlem3  16759  bj-inf2vnlem4  16760  bj-nn0sucALT  16765  bj-findis  16766  3dom  16779  trilpolemcl  16838