Theorem eleq1 2294

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 2241	. . . 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 1873	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2227	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2227	. 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 2202

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 2213

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

This theorem is referenced by:  eleq12  2296  eleq1i  2297  eleq1d  2300  eleq1a  2303  cleqh  2331  nelneq  2332  clelsb1  2336  nfcjust  2363  cleqf  2400  nelne2  2494  neleq1  2502  rgen2a  2587  cbvralf  2759  cbvrexf  2760  cbvreu  2766  cbvrab  2801  eqvisset  2814  ceqsralt  2831  vtoclgaf  2870  vtocl2gaf  2872  vtocl3gaf  2874  rspct  2904  rspc  2905  rspce  2906  rspc2gv  2923  ceqsrexv  2937  ceqsrexbv  2938  clel2  2940  elabgt  2948  elabgf  2949  elrabi  2960  elrabf  2961  elrab3t  2962  ralab2  2971  rexab2  2973  mo2icl  2986  morex  2991  reu2  2995  reu6  2996  rmo4  3000  reu8  3003  reuind  3012  nelrdva  3014  ru  3031  dfsbcq  3034  dfsbcq2  3035  sbc8g  3040  sbcel1v  3095  rmob  3126  difjust  3202  unjust  3204  injust  3206  eldif  3210  dfss2f  3219  uniiunlem  3318  elun  3350  elin  3392  rabn0m  3524  disjne  3550  r19.3rm  3585  r19.9rmv  3588  raaanlem  3601  raaan  3602  elif  3621  ifmdc  3652  elpwg  3664  elpr2  3695  elsn2g  3706  rabsn  3740  tpid3g  3791  snssb  3811  snssgOLD  3814  difsn  3815  sssnm  3842  opeq1  3867  opeq2  3868  eluni  3901  elunii  3903  eluniab  3910  elint  3939  elintg  3941  elintab  3944  elintrabg  3946  intss1  3948  eliun  3979  eliin  3980  dfiunv2  4011  opabss  4158  cbvmpt  4189  trel  4199  trss  4201  ssex  4231  intnexr  4246  intexabim  4247  exmidel  4301  euabex  4323  elopab  4358  opelopab2a  4365  frirrg  4453  tz7.2  4457  ordelord  4484  onm  4504  ralxfr2d  4567  rexxfr2d  4568  rabxfrd  4572  reuhypd  4574  ordtriexmid  4625  ontriexmidim  4626  ordtri2orexmid  4627  ontr2exmid  4629  onsucsssucexmid  4631  onsucelsucexmid  4634  ordsucunielexmid  4635  regexmidlem1  4637  elirr  4645  nordeq  4648  sucprcreg  4653  en2lp  4658  ordsoexmid  4666  ordsuc  4667  onsucuni2  4668  tfis  4687  peano2  4699  findes  4707  limom  4718  opelxp  4761  opeliunxp  4787  opbrop  4811  ssrel  4820  ssrel2  4822  ssrelrel  4832  relopabi  4861  eliunxp  4875  opeliunxp2  4876  ideqg  4887  reldmm  4956  dmmrnm  4957  dmxpm  4958  elreldm  4964  elrnmptg  4990  elres  5055  resiexg  5064  dfres2  5071  imai  5099  elimasng  5111  issref  5126  xpmlem  5164  xpm  5165  elxp4  5231  elxp5  5232  unielrel  5271  relcnvexb  5283  dmfex  5535  funfveu  5661  funimass4  5705  fvelimab  5711  ssimaex  5716  fvopab3g  5728  fvopab3ig  5729  fvmptssdm  5740  chfnrn  5767  fvelrn  5786  fmpt  5805  ffnfv  5813  fmptco  5821  elunirn  5917  f1elima  5924  cbvriota  5993  acexmidlemab  6022  acexmidlemcase  6023  cbvmpox  6109  eloprabga  6118  resoprab  6127  elrnmpo  6145  ov  6151  ovig  6153  ov6g  6170  ovg  6171  ovelrn  6181  caovimo  6226  fo1stresm  6333  fo2ndresm  6334  elxp6  6341  unielxp  6346  eqop2  6350  dfoprab4  6364  dfoprab4f  6365  fmpox  6374  1stconst  6395  2ndconst  6396  f1o2ndf1  6402  xporderlem  6405  f1od2  6409  disjxp1  6410  opeliunxp2f  6447  dftpos3  6471  dftpos4  6472  tpostpos  6473  smoel  6509  tfr1onlemaccex  6557  tfrcllemaccex  6570  tfrcl  6573  frecabcl  6608  frecsuc  6616  nntri3or  6704  nntri3  6708  nndcel  6711  riinerm  6820  th3qlem1  6849  mapsncnv  6907  elixpsn  6947  dom2lem  6988  fiprc  7033  xpsnen  7048  phplem3g  7085  phpelm  7096  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  elssdc  7137  inffiexmid  7141  undifdcss  7158  opabfi  7175  snon0  7177  f1dmvrnfibi  7186  f1vrnfibi  7187  suppeqfsuppbi  7220  ordiso2  7294  ctssdclemn0  7369  ctssdc  7372  enumct  7374  nnnninf  7385  nnnninfeq  7387  nninfisollemne  7390  nninfisol  7392  finomni  7399  exmidlpo  7402  pr2cv1  7460  acneq  7477  finacn  7479  acfun  7482  exmidontriimlem3  7498  exmidontriimlem4  7499  pw1ne1  7507  onntri35  7515  exmidapne  7539  ccfunen  7543  cc2lem  7545  elni2  7594  recexnq  7670  recmulnqg  7671  enq0enq  7711  enq0sym  7712  enq0ref  7713  enq0tr  7714  enq0breq  7716  nqnq0pi  7718  nqnq0  7721  prop  7755  prcdnql  7764  prcunqu  7765  prubl  7766  prltlu  7767  prnmaxl  7768  prnminu  7769  prdisj  7772  prarloc  7783  genipv  7789  genpelvl  7792  genpelvu  7793  genprndl  7801  genprndu  7802  distrlem5prl  7866  distrlem5pru  7867  ltexprlemm  7880  ltexprlemdisj  7886  ltexprlemloc  7887  ltexprlemrl  7890  ltexprlemru  7892  aptiprleml  7919  aptiprlemu  7920  archpr  7923  cauappcvgprlemm  7925  cauappcvgprlemladdfu  7934  cauappcvgprlemladdfl  7935  caucvgprlemm  7948  caucvgprlemladdfu  7957  caucvgprprlemmu  7975  elreal2  8110  ltresr  8119  axcnre  8161  axpre-suploclemres  8181  0re  8239  renepnf  8286  renemnf  8287  ltxrlt  8304  eqlei2  8333  0cnALT  8428  sup3exmid  9196  nn1suc  9221  nnne0  9230  xnn0xr  9531  nn0nepnf  9534  elz  9542  elnn0z  9553  elz2  9612  uzind4s  9885  elnn1uz2  9902  qre  9920  elpqb  9945  xnn0lenn0nn0  10161  xsubge0  10177  xposdif  10178  xleaddadd  10183  fzsn  10363  fz1sbc  10393  elfzp12  10396  fzm1  10397  fz01or  10408  fvinim0ffz  10550  suprzubdc  10559  zsupssdc  10561  xqltnle  10590  flqidz  10609  ceilqidz  10641  modqmuladdnn0  10693  frec2uzrand  10730  frecuzrdgtcl  10737  fzfig  10755  seq3fveq2  10800  seqfveq2g  10802  seq3shft2  10806  seqshft2g  10807  monoord  10810  seq3split  10813  seqsplitg  10814  iseqf1olemqval  10825  seq3id2  10851  seqhomog  10855  1exp  10893  bcval  11074  hashennn  11105  zfz1isolem1  11167  zfz1iso  11168  seq3coll  11169  iswrdiz  11186  0wrd0  11205  lswlgt0cl  11232  ccatval1  11240  ccatval2  11241  ccatalpha  11256  ccatrcl1  11257  wrdl1s1  11273  ccats1val2  11283  wrd2ind  11370  pfxccatin12lem3  11379  pfxccatid  11388  reuccatpfxs1lem  11393  shftlem  11456  shftfibg  11460  shftfib  11463  shftfn  11464  2shfti  11471  rexuz3  11630  sqrt0rlem  11643  cau3  11755  negfi  11868  sumdc  11998  sumrbdclem  12018  summodclem2a  12022  fisumss  12033  prodrbdclem  12212  prodmodclem2a  12217  fprodssdc  12231  fprodsplit1f  12275  ef0lem  12301  odd2np1  12514  even2n  12515  oddnn02np1  12521  oddge22np1  12522  evennn02n  12523  evennn2n  12524  nn0enne  12543  divalgmod  12568  uzwodc  12688  lcmgcdlem  12729  cncongr1  12755  1nprm  12766  isprm2  12769  dvdsnprmd  12777  prmdc  12782  exprmfct  12790  nprmdvds1  12792  coprm  12796  prmdiveq  12888  prm23lt5  12916  pcpre1  12945  pc2dvds  12983  pcz  12985  pcmpt  12996  qexpz  13005  4sqlem2  13042  4sqlem19  13062  ennnfonelemhom  13116  ctiunctlemudc  13138  ssnnctlemct  13147  nninfdclemcl  13149  imasaddfnlemg  13477  ismgmid  13540  isgrpid2  13703  mhmlem  13781  eqgval  13890  dvdsrcl2  14194  nzrunit  14283  lringuplu  14291  dvdsrzring  14699  znrrg  14756  mplsubgfilemm  14799  fiinopn  14815  istopon  14824  basis2  14859  eltg3  14868  tg2  14871  tgidm  14885  bastop  14886  bastop2  14895  topnex  14897  isopn3  14936  tgrest  14980  cnpval  15009  lmbr  15024  cnconst  15045  txbas  15069  uptx  15085  txdis1cn  15089  cnmpt12  15098  cnmpt22  15105  hmeocnvb  15129  xblm  15228  isxms2  15263  mopni  15293  blssioo  15364  dedekindeulemuub  15428  dedekindeulemeu  15433  dedekindicclemuub  15437  dedekindicclemeu  15442  ivthinclemlm  15445  ivthinclemum  15446  ivthreinc  15456  pellexlem3  15793  lgsfvalg  15824  lgsval2lem  15829  lgsdir2lem2  15848  gausslemma2dlem1a  15877  gausslemma2dlem4  15883  gausslemma2dlem6  15886  2lgslem1b  15908  2lgs  15923  2lgsoddprmlem2  15925  2lgsoddprmlem3  15930  2sqlem2  15934  2sqlem6  15939  2sqlem7  15940  2sqlem10  15944  vtxvalg  15957  iedgvalg  15958  umgredg  16086  upgrpredgv  16087  usgredg2vlem2  16164  ushgredgedg  16167  ushgredgedgloop  16169  griedg0ssusgr  16192  uhgrspansubgrlem  16217  vtxdgfifival  16232  iswlk  16264  upgrwlkvtxedg  16305  isclwwlknx  16357  clwwlkn1loopb  16361  clwwlknonex2lem1  16378  elabgf0  16495  bj-rspgt  16504  cbvrald  16506  decidi  16513  sumdc2  16517  bdssex  16618  bj-inex  16623  bj-intnexr  16625  bj-unexg  16637  bj-d0clsepcl  16641  bj-nnelirr  16669  bj-nn0suc  16680  bj-inf2vnlem1  16686  bj-inf2vnlem2  16687  bj-inf2vnlem3  16688  bj-inf2vnlem4  16689  bj-nn0sucALT  16694  bj-findis  16695  3dom  16708  trilpolemcl  16769