Theorem eleq1 2256

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 2203	. . . 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 1836	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2189	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2189	. 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 1364   E.wex 1503   e. wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eleq12  2258  eleq1i  2259  eleq1d  2262  eleq1a  2265  cleqh  2293  nelneq  2294  clelsb1  2298  nfcjust  2324  cleqf  2361  nelne2  2455  neleq1  2463  rgen2a  2548  cbvralf  2718  cbvrexf  2719  cbvreu  2724  cbvrab  2758  eqvisset  2770  ceqsralt  2787  vtoclgaf  2826  vtocl2gaf  2828  vtocl3gaf  2830  rspct  2858  rspc  2859  rspce  2860  rspc2gv  2877  ceqsrexv  2891  ceqsrexbv  2892  clel2  2894  elabgt  2902  elabgf  2903  elrabi  2914  elrabf  2915  elrab3t  2916  ralab2  2925  rexab2  2927  mo2icl  2940  morex  2945  reu2  2949  reu6  2950  rmo4  2954  reu8  2957  reuind  2966  nelrdva  2968  ru  2985  dfsbcq  2988  dfsbcq2  2989  sbc8g  2994  sbcel1v  3049  rmob  3079  difjust  3155  unjust  3157  injust  3159  eldif  3163  dfss2f  3171  uniiunlem  3269  elun  3301  elin  3343  rabn0m  3475  disjne  3501  r19.3rm  3536  r19.9rmv  3539  raaanlem  3552  raaan  3553  ifmdc  3598  elpwg  3610  elpr2  3641  elsn2g  3652  rabsn  3686  tpid3g  3734  snssb  3752  snssgOLD  3755  difsn  3756  sssnm  3781  opeq1  3805  opeq2  3806  eluni  3839  elunii  3841  eluniab  3848  elint  3877  elintg  3879  elintab  3882  elintrabg  3884  intss1  3886  eliun  3917  eliin  3918  dfiunv2  3949  opabss  4094  cbvmpt  4125  trel  4135  trss  4137  ssex  4167  intnexr  4181  intexabim  4182  exmidel  4235  euabex  4255  elopab  4289  opelopab2a  4296  frirrg  4382  tz7.2  4386  ordelord  4413  onm  4433  ralxfr2d  4496  rexxfr2d  4497  rabxfrd  4501  reuhypd  4503  ordtriexmid  4554  ontriexmidim  4555  ordtri2orexmid  4556  ontr2exmid  4558  onsucsssucexmid  4560  onsucelsucexmid  4563  ordsucunielexmid  4564  regexmidlem1  4566  elirr  4574  nordeq  4577  sucprcreg  4582  en2lp  4587  ordsoexmid  4595  ordsuc  4596  onsucuni2  4597  tfis  4616  peano2  4628  findes  4636  limom  4647  opelxp  4690  opeliunxp  4715  opbrop  4739  ssrel  4748  ssrel2  4750  ssrelrel  4760  relopabi  4788  eliunxp  4802  opeliunxp2  4803  ideqg  4814  dmmrnm  4882  dmxpm  4883  elreldm  4889  elrnmptg  4915  elres  4979  resiexg  4988  dfres2  4995  imai  5022  elimasng  5034  issref  5049  xpmlem  5087  xpm  5088  elxp4  5154  elxp5  5155  unielrel  5194  relcnvexb  5206  dmfex  5444  funfveu  5568  funimass4  5608  fvelimab  5614  ssimaex  5619  fvopab3g  5631  fvopab3ig  5632  fvmptssdm  5643  chfnrn  5670  fvelrn  5690  fmpt  5709  ffnfv  5717  fmptco  5725  elunirn  5810  f1elima  5817  cbvriota  5885  acexmidlemab  5913  acexmidlemcase  5914  cbvmpox  5997  eloprabga  6006  resoprab  6015  elrnmpo  6033  ov  6039  ovig  6041  ov6g  6058  ovg  6059  ovelrn  6069  caovimo  6114  fo1stresm  6216  fo2ndresm  6217  elxp6  6224  unielxp  6229  eqop2  6233  dfoprab4  6247  dfoprab4f  6248  fmpox  6255  1stconst  6276  2ndconst  6277  f1o2ndf1  6283  xporderlem  6286  f1od2  6290  disjxp1  6291  opeliunxp2f  6293  dftpos3  6317  dftpos4  6318  tpostpos  6319  smoel  6355  tfr1onlemaccex  6403  tfrcllemaccex  6416  tfrcl  6419  frecabcl  6454  frecsuc  6462  nntri3or  6548  nntri3  6552  nndcel  6555  riinerm  6664  th3qlem1  6693  mapsncnv  6751  elixpsn  6791  dom2lem  6828  fiprc  6871  xpsnen  6877  phplem3g  6914  phpelm  6924  ssfiexmid  6934  domfiexmid  6936  inffiexmid  6964  undifdcss  6981  opabfi  6994  snon0  6996  f1dmvrnfibi  7005  f1vrnfibi  7006  ordiso2  7096  ctssdclemn0  7171  ctssdc  7174  enumct  7176  nnnninf  7187  nnnninfeq  7189  nninfisollemne  7192  nninfisol  7194  finomni  7201  exmidlpo  7204  acfun  7269  exmidontriimlem3  7285  exmidontriimlem4  7286  pw1ne1  7291  onntri35  7299  exmidapne  7322  ccfunen  7326  cc2lem  7328  elni2  7376  recexnq  7452  recmulnqg  7453  enq0enq  7493  enq0sym  7494  enq0ref  7495  enq0tr  7496  enq0breq  7498  nqnq0pi  7500  nqnq0  7503  prop  7537  prcdnql  7546  prcunqu  7547  prubl  7548  prltlu  7549  prnmaxl  7550  prnminu  7551  prdisj  7554  prarloc  7565  genipv  7571  genpelvl  7574  genpelvu  7575  genprndl  7583  genprndu  7584  distrlem5prl  7648  distrlem5pru  7649  ltexprlemm  7662  ltexprlemdisj  7668  ltexprlemloc  7669  ltexprlemrl  7672  ltexprlemru  7674  aptiprleml  7701  aptiprlemu  7702  archpr  7705  cauappcvgprlemm  7707  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  caucvgprlemm  7730  caucvgprlemladdfu  7739  caucvgprprlemmu  7757  elreal2  7892  ltresr  7901  axcnre  7943  axpre-suploclemres  7963  0re  8021  renepnf  8069  renemnf  8070  ltxrlt  8087  eqlei2  8116  0cnALT  8211  sup3exmid  8978  nn1suc  9003  nnne0  9012  xnn0xr  9311  nn0nepnf  9314  elz  9322  elnn0z  9333  elz2  9391  uzind4s  9658  elnn1uz2  9675  qre  9693  elpqb  9718  xnn0lenn0nn0  9934  xsubge0  9950  xposdif  9951  xleaddadd  9956  fzsn  10135  fz1sbc  10165  elfzp12  10168  fzm1  10169  fz01or  10180  fvinim0ffz  10311  xqltnle  10339  flqidz  10358  ceilqidz  10390  modqmuladdnn0  10442  frec2uzrand  10479  frecuzrdgtcl  10486  fzfig  10504  seq3fveq2  10549  seqfveq2g  10551  seq3shft2  10555  seqshft2g  10556  monoord  10559  seq3split  10562  seqsplitg  10563  iseqf1olemqval  10574  seq3id2  10600  seqhomog  10604  1exp  10642  bcval  10823  hashennn  10854  zfz1isolem1  10914  zfz1iso  10915  seq3coll  10916  iswrdiz  10924  0wrd0  10943  shftlem  10963  shftfibg  10967  shftfib  10970  shftfn  10971  2shfti  10978  rexuz3  11137  sqrt0rlem  11150  cau3  11262  negfi  11374  sumdc  11504  sumrbdclem  11523  summodclem2a  11527  fisumss  11538  prodrbdclem  11717  prodmodclem2a  11722  fprodssdc  11736  fprodsplit1f  11780  ef0lem  11806  odd2np1  12017  even2n  12018  oddnn02np1  12024  oddge22np1  12025  evennn02n  12026  evennn2n  12027  nn0enne  12046  divalgmod  12071  suprzubdc  12092  zsupssdc  12094  uzwodc  12177  lcmgcdlem  12218  cncongr1  12244  1nprm  12255  isprm2  12258  dvdsnprmd  12266  prmdc  12271  exprmfct  12279  nprmdvds1  12281  coprm  12285  prmdiveq  12377  prm23lt5  12404  pcpre1  12433  pc2dvds  12471  pcz  12473  pcmpt  12484  qexpz  12493  4sqlem2  12530  4sqlem19  12550  ennnfonelemhom  12575  ctiunctlemudc  12597  ssnnctlemct  12606  nninfdclemcl  12608  imasaddfnlemg  12900  ismgmid  12963  isgrpid2  13115  mhmlem  13187  eqgval  13296  dvdsrcl2  13598  nzrunit  13687  lringuplu  13695  dvdsrzring  14102  znrrg  14159  fiinopn  14183  istopon  14192  basis2  14227  eltg3  14236  tg2  14239  tgidm  14253  bastop  14254  bastop2  14263  topnex  14265  isopn3  14304  tgrest  14348  cnpval  14377  lmbr  14392  cnconst  14413  txbas  14437  uptx  14453  txdis1cn  14457  cnmpt12  14466  cnmpt22  14473  hmeocnvb  14497  xblm  14596  isxms2  14631  mopni  14661  blssioo  14732  dedekindeulemuub  14796  dedekindeulemeu  14801  dedekindicclemuub  14805  dedekindicclemeu  14810  ivthinclemlm  14813  ivthinclemum  14814  ivthreinc  14824  lgsfvalg  15162  lgsval2lem  15167  lgsdir2lem2  15186  gausslemma2dlem1a  15215  gausslemma2dlem4  15221  gausslemma2dlem6  15224  2lgslem1b  15246  2lgs  15261  2lgsoddprmlem2  15263  2lgsoddprmlem3  15268  2sqlem2  15272  2sqlem6  15277  2sqlem7  15278  2sqlem10  15282  elabgf0  15339  bj-rspgt  15348  cbvrald  15350  decidi  15357  sumdc2  15361  bdssex  15464  bj-inex  15469  bj-intnexr  15471  bj-unexg  15483  bj-d0clsepcl  15487  bj-nnelirr  15515  bj-nn0suc  15526  bj-inf2vnlem1  15532  bj-inf2vnlem2  15533  bj-inf2vnlem3  15534  bj-inf2vnlem4  15535  bj-nn0sucALT  15540  bj-findis  15541  trilpolemcl  15597