Theorem eleq1 2259

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 2206	. . . 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 1839	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2192	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2192	. 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 1506   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

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

This theorem is referenced by:  eleq12  2261  eleq1i  2262  eleq1d  2265  eleq1a  2268  cleqh  2296  nelneq  2297  clelsb1  2301  nfcjust  2327  cleqf  2364  nelne2  2458  neleq1  2466  rgen2a  2551  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvrab  2761  eqvisset  2773  ceqsralt  2790  vtoclgaf  2829  vtocl2gaf  2831  vtocl3gaf  2833  rspct  2861  rspc  2862  rspce  2863  rspc2gv  2880  ceqsrexv  2894  ceqsrexbv  2895  clel2  2897  elabgt  2905  elabgf  2906  elrabi  2917  elrabf  2918  elrab3t  2919  ralab2  2928  rexab2  2930  mo2icl  2943  morex  2948  reu2  2952  reu6  2953  rmo4  2957  reu8  2960  reuind  2969  nelrdva  2971  ru  2988  dfsbcq  2991  dfsbcq2  2992  sbc8g  2997  sbcel1v  3052  rmob  3082  difjust  3158  unjust  3160  injust  3162  eldif  3166  dfss2f  3175  uniiunlem  3273  elun  3305  elin  3347  rabn0m  3479  disjne  3505  r19.3rm  3540  r19.9rmv  3543  raaanlem  3556  raaan  3557  ifmdc  3602  elpwg  3614  elpr2  3645  elsn2g  3656  rabsn  3690  tpid3g  3738  snssb  3756  snssgOLD  3759  difsn  3760  sssnm  3785  opeq1  3809  opeq2  3810  eluni  3843  elunii  3845  eluniab  3852  elint  3881  elintg  3883  elintab  3886  elintrabg  3888  intss1  3890  eliun  3921  eliin  3922  dfiunv2  3953  opabss  4098  cbvmpt  4129  trel  4139  trss  4141  ssex  4171  intnexr  4185  intexabim  4186  exmidel  4239  euabex  4259  elopab  4293  opelopab2a  4300  frirrg  4386  tz7.2  4390  ordelord  4417  onm  4437  ralxfr2d  4500  rexxfr2d  4501  rabxfrd  4505  reuhypd  4507  ordtriexmid  4558  ontriexmidim  4559  ordtri2orexmid  4560  ontr2exmid  4562  onsucsssucexmid  4564  onsucelsucexmid  4567  ordsucunielexmid  4568  regexmidlem1  4570  elirr  4578  nordeq  4581  sucprcreg  4586  en2lp  4591  ordsoexmid  4599  ordsuc  4600  onsucuni2  4601  tfis  4620  peano2  4632  findes  4640  limom  4651  opelxp  4694  opeliunxp  4719  opbrop  4743  ssrel  4752  ssrel2  4754  ssrelrel  4764  relopabi  4792  eliunxp  4806  opeliunxp2  4807  ideqg  4818  dmmrnm  4886  dmxpm  4887  elreldm  4893  elrnmptg  4919  elres  4983  resiexg  4992  dfres2  4999  imai  5026  elimasng  5038  issref  5053  xpmlem  5091  xpm  5092  elxp4  5158  elxp5  5159  unielrel  5198  relcnvexb  5210  dmfex  5450  funfveu  5574  funimass4  5614  fvelimab  5620  ssimaex  5625  fvopab3g  5637  fvopab3ig  5638  fvmptssdm  5649  chfnrn  5676  fvelrn  5696  fmpt  5715  ffnfv  5723  fmptco  5731  elunirn  5816  f1elima  5823  cbvriota  5891  acexmidlemab  5919  acexmidlemcase  5920  cbvmpox  6004  eloprabga  6013  resoprab  6022  elrnmpo  6040  ov  6046  ovig  6048  ov6g  6065  ovg  6066  ovelrn  6076  caovimo  6121  fo1stresm  6228  fo2ndresm  6229  elxp6  6236  unielxp  6241  eqop2  6245  dfoprab4  6259  dfoprab4f  6260  fmpox  6267  1stconst  6288  2ndconst  6289  f1o2ndf1  6295  xporderlem  6298  f1od2  6302  disjxp1  6303  opeliunxp2f  6305  dftpos3  6329  dftpos4  6330  tpostpos  6331  smoel  6367  tfr1onlemaccex  6415  tfrcllemaccex  6428  tfrcl  6431  frecabcl  6466  frecsuc  6474  nntri3or  6560  nntri3  6564  nndcel  6567  riinerm  6676  th3qlem1  6705  mapsncnv  6763  elixpsn  6803  dom2lem  6840  fiprc  6883  xpsnen  6889  phplem3g  6926  phpelm  6936  ssfiexmid  6946  domfiexmid  6948  inffiexmid  6976  undifdcss  6993  opabfi  7008  snon0  7010  f1dmvrnfibi  7019  f1vrnfibi  7020  ordiso2  7110  ctssdclemn0  7185  ctssdc  7188  enumct  7190  nnnninf  7201  nnnninfeq  7203  nninfisollemne  7206  nninfisol  7208  finomni  7215  exmidlpo  7218  acneq  7285  finacn  7287  acfun  7290  exmidontriimlem3  7306  exmidontriimlem4  7307  pw1ne1  7312  onntri35  7320  exmidapne  7343  ccfunen  7347  cc2lem  7349  elni2  7398  recexnq  7474  recmulnqg  7475  enq0enq  7515  enq0sym  7516  enq0ref  7517  enq0tr  7518  enq0breq  7520  nqnq0pi  7522  nqnq0  7525  prop  7559  prcdnql  7568  prcunqu  7569  prubl  7570  prltlu  7571  prnmaxl  7572  prnminu  7573  prdisj  7576  prarloc  7587  genipv  7593  genpelvl  7596  genpelvu  7597  genprndl  7605  genprndu  7606  distrlem5prl  7670  distrlem5pru  7671  ltexprlemm  7684  ltexprlemdisj  7690  ltexprlemloc  7691  ltexprlemrl  7694  ltexprlemru  7696  aptiprleml  7723  aptiprlemu  7724  archpr  7727  cauappcvgprlemm  7729  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  caucvgprlemm  7752  caucvgprlemladdfu  7761  caucvgprprlemmu  7779  elreal2  7914  ltresr  7923  axcnre  7965  axpre-suploclemres  7985  0re  8043  renepnf  8091  renemnf  8092  ltxrlt  8109  eqlei2  8138  0cnALT  8233  sup3exmid  9001  nn1suc  9026  nnne0  9035  xnn0xr  9334  nn0nepnf  9337  elz  9345  elnn0z  9356  elz2  9414  uzind4s  9681  elnn1uz2  9698  qre  9716  elpqb  9741  xnn0lenn0nn0  9957  xsubge0  9973  xposdif  9974  xleaddadd  9979  fzsn  10158  fz1sbc  10188  elfzp12  10191  fzm1  10192  fz01or  10203  fvinim0ffz  10334  suprzubdc  10343  zsupssdc  10345  xqltnle  10374  flqidz  10393  ceilqidz  10425  modqmuladdnn0  10477  frec2uzrand  10514  frecuzrdgtcl  10521  fzfig  10539  seq3fveq2  10584  seqfveq2g  10586  seq3shft2  10590  seqshft2g  10591  monoord  10594  seq3split  10597  seqsplitg  10598  iseqf1olemqval  10609  seq3id2  10635  seqhomog  10639  1exp  10677  bcval  10858  hashennn  10889  zfz1isolem1  10949  zfz1iso  10950  seq3coll  10951  iswrdiz  10959  0wrd0  10978  shftlem  10998  shftfibg  11002  shftfib  11005  shftfn  11006  2shfti  11013  rexuz3  11172  sqrt0rlem  11185  cau3  11297  negfi  11410  sumdc  11540  sumrbdclem  11559  summodclem2a  11563  fisumss  11574  prodrbdclem  11753  prodmodclem2a  11758  fprodssdc  11772  fprodsplit1f  11816  ef0lem  11842  odd2np1  12055  even2n  12056  oddnn02np1  12062  oddge22np1  12063  evennn02n  12064  evennn2n  12065  nn0enne  12084  divalgmod  12109  uzwodc  12229  lcmgcdlem  12270  cncongr1  12296  1nprm  12307  isprm2  12310  dvdsnprmd  12318  prmdc  12323  exprmfct  12331  nprmdvds1  12333  coprm  12337  prmdiveq  12429  prm23lt5  12457  pcpre1  12486  pc2dvds  12524  pcz  12526  pcmpt  12537  qexpz  12546  4sqlem2  12583  4sqlem19  12603  ennnfonelemhom  12657  ctiunctlemudc  12679  ssnnctlemct  12688  nninfdclemcl  12690  imasaddfnlemg  13016  ismgmid  13079  isgrpid2  13242  mhmlem  13320  eqgval  13429  dvdsrcl2  13731  nzrunit  13820  lringuplu  13828  dvdsrzring  14235  znrrg  14292  fiinopn  14324  istopon  14333  basis2  14368  eltg3  14377  tg2  14380  tgidm  14394  bastop  14395  bastop2  14404  topnex  14406  isopn3  14445  tgrest  14489  cnpval  14518  lmbr  14533  cnconst  14554  txbas  14578  uptx  14594  txdis1cn  14598  cnmpt12  14607  cnmpt22  14614  hmeocnvb  14638  xblm  14737  isxms2  14772  mopni  14802  blssioo  14873  dedekindeulemuub  14937  dedekindeulemeu  14942  dedekindicclemuub  14946  dedekindicclemeu  14951  ivthinclemlm  14954  ivthinclemum  14955  ivthreinc  14965  lgsfvalg  15330  lgsval2lem  15335  lgsdir2lem2  15354  gausslemma2dlem1a  15383  gausslemma2dlem4  15389  gausslemma2dlem6  15392  2lgslem1b  15414  2lgs  15429  2lgsoddprmlem2  15431  2lgsoddprmlem3  15436  2sqlem2  15440  2sqlem6  15445  2sqlem7  15446  2sqlem10  15450  elabgf0  15507  bj-rspgt  15516  cbvrald  15518  decidi  15525  sumdc2  15529  bdssex  15632  bj-inex  15637  bj-intnexr  15639  bj-unexg  15651  bj-d0clsepcl  15655  bj-nnelirr  15683  bj-nn0suc  15694  bj-inf2vnlem1  15700  bj-inf2vnlem2  15701  bj-inf2vnlem3  15702  bj-inf2vnlem4  15703  bj-nn0sucALT  15708  bj-findis  15709  trilpolemcl  15768