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 1397   E.wex 1540   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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  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  2362  cleqf  2399  nelne2  2493  neleq1  2501  rgen2a  2586  cbvralf  2758  cbvrexf  2759  cbvreu  2765  cbvrab  2800  eqvisset  2813  ceqsralt  2830  vtoclgaf  2869  vtocl2gaf  2871  vtocl3gaf  2873  rspct  2903  rspc  2904  rspce  2905  rspc2gv  2922  ceqsrexv  2936  ceqsrexbv  2937  clel2  2939  elabgt  2947  elabgf  2948  elrabi  2959  elrabf  2960  elrab3t  2961  ralab2  2970  rexab2  2972  mo2icl  2985  morex  2990  reu2  2994  reu6  2995  rmo4  2999  reu8  3002  reuind  3011  nelrdva  3013  ru  3030  dfsbcq  3033  dfsbcq2  3034  sbc8g  3039  sbcel1v  3094  rmob  3125  difjust  3201  unjust  3203  injust  3205  eldif  3209  dfss2f  3218  uniiunlem  3316  elun  3348  elin  3390  rabn0m  3522  disjne  3548  r19.3rm  3583  r19.9rmv  3586  raaanlem  3599  raaan  3600  elif  3617  ifmdc  3648  elpwg  3660  elpr2  3691  elsn2g  3702  rabsn  3736  tpid3g  3787  snssb  3806  snssgOLD  3809  difsn  3810  sssnm  3837  opeq1  3862  opeq2  3863  eluni  3896  elunii  3898  eluniab  3905  elint  3934  elintg  3936  elintab  3939  elintrabg  3941  intss1  3943  eliun  3974  eliin  3975  dfiunv2  4006  opabss  4153  cbvmpt  4184  trel  4194  trss  4196  ssex  4226  intnexr  4241  intexabim  4242  exmidel  4295  euabex  4317  elopab  4352  opelopab2a  4359  frirrg  4447  tz7.2  4451  ordelord  4478  onm  4498  ralxfr2d  4561  rexxfr2d  4562  rabxfrd  4566  reuhypd  4568  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  ordsucunielexmid  4629  regexmidlem1  4631  elirr  4639  nordeq  4642  sucprcreg  4647  en2lp  4652  ordsoexmid  4660  ordsuc  4661  onsucuni2  4662  tfis  4681  peano2  4693  findes  4701  limom  4712  opelxp  4755  opeliunxp  4781  opbrop  4805  ssrel  4814  ssrel2  4816  ssrelrel  4826  relopabi  4855  eliunxp  4869  opeliunxp2  4870  ideqg  4881  reldmm  4950  dmmrnm  4951  dmxpm  4952  elreldm  4958  elrnmptg  4984  elres  5049  resiexg  5058  dfres2  5065  imai  5092  elimasng  5104  issref  5119  xpmlem  5157  xpm  5158  elxp4  5224  elxp5  5225  unielrel  5264  relcnvexb  5276  dmfex  5526  funfveu  5652  funimass4  5696  fvelimab  5702  ssimaex  5707  fvopab3g  5719  fvopab3ig  5720  fvmptssdm  5731  chfnrn  5758  fvelrn  5778  fmpt  5797  ffnfv  5805  fmptco  5813  elunirn  5907  f1elima  5914  cbvriota  5983  acexmidlemab  6012  acexmidlemcase  6013  cbvmpox  6099  eloprabga  6108  resoprab  6117  elrnmpo  6135  ov  6141  ovig  6143  ov6g  6160  ovg  6161  ovelrn  6171  caovimo  6216  fo1stresm  6324  fo2ndresm  6325  elxp6  6332  unielxp  6337  eqop2  6341  dfoprab4  6355  dfoprab4f  6356  fmpox  6365  1stconst  6386  2ndconst  6387  f1o2ndf1  6393  xporderlem  6396  f1od2  6400  disjxp1  6401  opeliunxp2f  6404  dftpos3  6428  dftpos4  6429  tpostpos  6430  smoel  6466  tfr1onlemaccex  6514  tfrcllemaccex  6527  tfrcl  6530  frecabcl  6565  frecsuc  6573  nntri3or  6661  nntri3  6665  nndcel  6668  riinerm  6777  th3qlem1  6806  mapsncnv  6864  elixpsn  6904  dom2lem  6945  fiprc  6990  xpsnen  7005  phplem3g  7042  phpelm  7053  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  elssdc  7094  inffiexmid  7098  undifdcss  7115  opabfi  7132  snon0  7134  f1dmvrnfibi  7143  f1vrnfibi  7144  ordiso2  7234  ctssdclemn0  7309  ctssdc  7312  enumct  7314  nnnninf  7325  nnnninfeq  7327  nninfisollemne  7330  nninfisol  7332  finomni  7339  exmidlpo  7342  pr2cv1  7400  acneq  7417  finacn  7419  acfun  7422  exmidontriimlem3  7438  exmidontriimlem4  7439  pw1ne1  7447  onntri35  7455  exmidapne  7479  ccfunen  7483  cc2lem  7485  elni2  7534  recexnq  7610  recmulnqg  7611  enq0enq  7651  enq0sym  7652  enq0ref  7653  enq0tr  7654  enq0breq  7656  nqnq0pi  7658  nqnq0  7661  prop  7695  prcdnql  7704  prcunqu  7705  prubl  7706  prltlu  7707  prnmaxl  7708  prnminu  7709  prdisj  7712  prarloc  7723  genipv  7729  genpelvl  7732  genpelvu  7733  genprndl  7741  genprndu  7742  distrlem5prl  7806  distrlem5pru  7807  ltexprlemm  7820  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  aptiprleml  7859  aptiprlemu  7860  archpr  7863  cauappcvgprlemm  7865  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  caucvgprlemm  7888  caucvgprlemladdfu  7897  caucvgprprlemmu  7915  elreal2  8050  ltresr  8059  axcnre  8101  axpre-suploclemres  8121  0re  8179  renepnf  8227  renemnf  8228  ltxrlt  8245  eqlei2  8274  0cnALT  8369  sup3exmid  9137  nn1suc  9162  nnne0  9171  xnn0xr  9470  nn0nepnf  9473  elz  9481  elnn0z  9492  elz2  9551  uzind4s  9824  elnn1uz2  9841  qre  9859  elpqb  9884  xnn0lenn0nn0  10100  xsubge0  10116  xposdif  10117  xleaddadd  10122  fzsn  10301  fz1sbc  10331  elfzp12  10334  fzm1  10335  fz01or  10346  fvinim0ffz  10488  suprzubdc  10497  zsupssdc  10499  xqltnle  10528  flqidz  10547  ceilqidz  10579  modqmuladdnn0  10631  frec2uzrand  10668  frecuzrdgtcl  10675  fzfig  10693  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  iseqf1olemqval  10763  seq3id2  10789  seqhomog  10793  1exp  10831  bcval  11012  hashennn  11043  zfz1isolem1  11105  zfz1iso  11106  seq3coll  11107  iswrdiz  11124  0wrd0  11143  lswlgt0cl  11170  ccatval1  11178  ccatval2  11179  ccatalpha  11194  ccatrcl1  11195  wrdl1s1  11211  ccats1val2  11221  wrd2ind  11308  pfxccatin12lem3  11317  pfxccatid  11326  reuccatpfxs1lem  11331  shftlem  11394  shftfibg  11398  shftfib  11401  shftfn  11402  2shfti  11409  rexuz3  11568  sqrt0rlem  11581  cau3  11693  negfi  11806  sumdc  11936  sumrbdclem  11956  summodclem2a  11960  fisumss  11971  prodrbdclem  12150  prodmodclem2a  12155  fprodssdc  12169  fprodsplit1f  12213  ef0lem  12239  odd2np1  12452  even2n  12453  oddnn02np1  12459  oddge22np1  12460  evennn02n  12461  evennn2n  12462  nn0enne  12481  divalgmod  12506  uzwodc  12626  lcmgcdlem  12667  cncongr1  12693  1nprm  12704  isprm2  12707  dvdsnprmd  12715  prmdc  12720  exprmfct  12728  nprmdvds1  12730  coprm  12734  prmdiveq  12826  prm23lt5  12854  pcpre1  12883  pc2dvds  12921  pcz  12923  pcmpt  12934  qexpz  12943  4sqlem2  12980  4sqlem19  13000  ennnfonelemhom  13054  ctiunctlemudc  13076  ssnnctlemct  13085  nninfdclemcl  13087  imasaddfnlemg  13415  ismgmid  13478  isgrpid2  13641  mhmlem  13719  eqgval  13828  dvdsrcl2  14132  nzrunit  14221  lringuplu  14229  dvdsrzring  14636  znrrg  14693  mplsubgfilemm  14731  fiinopn  14747  istopon  14756  basis2  14791  eltg3  14800  tg2  14803  tgidm  14817  bastop  14818  bastop2  14827  topnex  14829  isopn3  14868  tgrest  14912  cnpval  14941  lmbr  14956  cnconst  14977  txbas  15001  uptx  15017  txdis1cn  15021  cnmpt12  15030  cnmpt22  15037  hmeocnvb  15061  xblm  15160  isxms2  15195  mopni  15225  blssioo  15296  dedekindeulemuub  15360  dedekindeulemeu  15365  dedekindicclemuub  15369  dedekindicclemeu  15374  ivthinclemlm  15377  ivthinclemum  15378  ivthreinc  15388  lgsfvalg  15753  lgsval2lem  15758  lgsdir2lem2  15777  gausslemma2dlem1a  15806  gausslemma2dlem4  15812  gausslemma2dlem6  15815  2lgslem1b  15837  2lgs  15852  2lgsoddprmlem2  15854  2lgsoddprmlem3  15859  2sqlem2  15863  2sqlem6  15868  2sqlem7  15869  2sqlem10  15873  vtxvalg  15886  iedgvalg  15887  umgredg  16015  upgrpredgv  16016  usgredg2vlem2  16093  ushgredgedg  16096  ushgredgedgloop  16098  griedg0ssusgr  16121  uhgrspansubgrlem  16146  vtxdgfifival  16161  iswlk  16193  upgrwlkvtxedg  16234  isclwwlknx  16286  clwwlkn1loopb  16290  clwwlknonex2lem1  16307  elabgf0  16424  bj-rspgt  16433  cbvrald  16435  decidi  16442  sumdc2  16446  bdssex  16548  bj-inex  16553  bj-intnexr  16555  bj-unexg  16567  bj-d0clsepcl  16571  bj-nnelirr  16599  bj-nn0suc  16610  bj-inf2vnlem1  16616  bj-inf2vnlem2  16617  bj-inf2vnlem3  16618  bj-inf2vnlem4  16619  bj-nn0sucALT  16624  bj-findis  16625  3dom  16638  trilpolemcl  16692