Theorem eleq1 2301

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 2248	. . . 4 |- ( A = B -> ( x = A <-> x = B ) )
2	1	anbi1d 469	. . 3 |- ( A = B -> ( ( x = A /\ x e. C ) <-> ( x = B /\ x e. C ) ) )
3	2	exbidv 1878	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2234	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2234	. 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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   E.wex 1545   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleq12  2303  eleq1i  2304  eleq1d  2307  eleq1a  2310  cleqh  2338  nelneq  2339  clelsb1  2343  nfcjust  2380  cleqf  2417  nelne2  2511  neleq1  2519  rgen2a  2604  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvrab  2819  eqvisset  2832  ceqsralt  2849  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  rspct  2922  rspc  2923  rspce  2924  rspc2gv  2942  ceqsrexv  2956  ceqsrexbv  2957  clel2  2959  elabgt  2967  elabgf  2968  elrabi  2979  elrabf  2980  elrab3t  2981  ralab2  2990  rexab2  2992  mo2icl  3005  morex  3010  reu2  3014  reu6  3015  rmo4  3019  reu8  3022  reuind  3031  nelrdva  3033  ru  3050  dfsbcq  3053  dfsbcq2  3054  sbc8g  3059  sbcel1v  3114  rmob  3145  difjust  3221  unjust  3223  injust  3225  eldif  3229  dfssf  3238  dfss2f  3239  uniiunlem  3338  elun  3370  elin  3412  rabn0m  3549  disjne  3578  r19.3rm  3616  r19.9rmv  3619  raaanlem  3632  raaan  3633  elif  3652  ifmdc  3683  elpwg  3696  elpr2  3731  elsn2g  3742  rabsn  3776  tpid3g  3828  snssb  3848  snssgOLD  3851  difsn  3852  sssnm  3879  opeq1  3904  opeq2  3905  eluni  3938  elunii  3940  eluniab  3947  elint  3976  elintg  3978  elintab  3981  elintrabg  3983  intss1  3985  eliun  4016  eliin  4017  dfiunv2  4048  opabss  4196  cbvmpt  4228  trel  4238  trss  4240  ssex  4272  intnexr  4289  intexabim  4290  exmidel  4344  euabex  4367  elopab  4402  opelopab2a  4409  frirrg  4497  tz7.2  4501  ordelord  4528  onm  4548  ralxfr2d  4612  rexxfr2d  4613  rabxfrd  4617  reuhypd  4619  ordtriexmid  4670  ontriexmidim  4671  ordtri2orexmid  4672  ontr2exmid  4674  onsucsssucexmid  4676  onsucelsucexmid  4679  ordsucunielexmid  4680  regexmidlem1  4682  elirr  4690  nordeq  4693  sucprcreg  4698  en2lp  4703  ordsoexmid  4711  ordsuc  4712  onsucuni2  4713  tfis  4732  peano2  4744  findes  4752  limom  4763  opelxp  4806  opeliunxp  4832  opbrop  4856  ssrel  4865  ssrel2  4867  ssrelrel  4877  relopabi  4907  eliunxp  4921  opeliunxp2  4922  ideqg  4933  reldmm  5002  dmmrnm  5003  dmxpm  5004  elreldm  5010  elrnmptg  5036  elres  5101  resiexg  5111  dfres2  5118  imai  5146  elimasng  5158  issref  5173  xpmlem  5211  xpm  5212  elxp4  5278  elxp5  5279  unielrel  5318  relcnvexb  5330  dmfex  5585  funfveu  5711  funimass4  5756  fvelimab  5762  ssimaex  5767  fvopab3g  5781  fvopab3ig  5782  fvmptssdm  5793  chfnrn  5823  fvelrn  5842  fmpt  5861  ffnfv  5869  fmptco  5877  elunirn  5975  f1elima  5982  cbvriota  6053  acexmidlemab  6082  acexmidlemcase  6083  cbvmpox  6169  eloprabga  6178  resoprab  6187  elrnmpo  6205  ov  6211  ovig  6213  ov6g  6230  ovg  6231  ovelrn  6241  caovimo  6286  abrexss  6362  fo1stresm  6399  fo2ndresm  6400  elxp6  6407  unielxp  6412  eqop2  6416  dfoprab4  6430  dfoprab4f  6431  fmpox  6440  1stconst  6461  2ndconst  6462  f1o2ndf1  6468  xporderlem  6471  f1od2  6475  disjxp1  6476  opeliunxp2f  6513  dftpos3  6537  dftpos4  6538  tpostpos  6539  smoel  6575  tfr1onlemaccex  6623  tfrcllemaccex  6636  tfrcl  6639  frecabcl  6674  frecsuc  6682  nntri3or  6770  nntri3  6774  nndcel  6777  riinerm  6886  th3qlem1  6915  mapsncnv  6981  elixpsn  7021  dom2lem  7062  fiprc  7108  xpsnen  7123  phplem3g  7161  phpelm  7172  ssfiexmid  7182  ssfiexmidt  7184  domfiexmid  7186  elssdc  7213  inffiexmid  7217  undifdcss  7234  opabfi  7251  snon0  7253  f1dmvrnfibi  7262  f1vrnfibi  7263  relresfin  7268  suppeqfsuppbi  7300  ordiso2  7381  ctssdclemn0  7456  ctssdc  7459  enumct  7461  nnnninf  7472  nnnninfeq  7474  nninfisollemne  7477  nninfisol  7479  finomni  7486  exmidlpo  7489  pr2cv1  7547  acneq  7564  finacn  7566  acfun  7569  exmidontriimlem3  7585  exmidontriimlem4  7586  pw1ne1  7594  onntri35  7602  exmidapne  7632  ccfunen  7636  cc2lem  7638  elni2  7687  recexnq  7763  recmulnqg  7764  enq0enq  7804  enq0sym  7805  enq0ref  7806  enq0tr  7807  enq0breq  7809  nqnq0pi  7811  nqnq0  7814  prop  7848  prcdnql  7857  prcunqu  7858  prubl  7859  prltlu  7860  prnmaxl  7861  prnminu  7862  prdisj  7865  prarloc  7876  genipv  7882  genpelvl  7885  genpelvu  7886  genprndl  7894  genprndu  7895  distrlem5prl  7959  distrlem5pru  7960  ltexprlemm  7973  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  aptiprleml  8012  aptiprlemu  8013  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  caucvgprlemm  8041  caucvgprlemladdfu  8050  caucvgprprlemmu  8068  elreal2  8203  ltresr  8212  axcnre  8254  axpre-suploclemres  8274  0re  8332  renepnf  8379  renemnf  8380  ltxrlt  8397  eqlei2  8427  0cnALT  8523  sup3exmid  9295  nn1suc  9332  nnne0  9341  xnn0xr  9646  nn0nepnf  9649  elz  9657  elnn0z  9668  elz2  9727  uzind4s  10006  elnn1uz2  10023  qre  10041  elpqb  10067  xnn0lenn0nn0  10284  xsubge0  10300  xposdif  10301  xleaddadd  10306  fzsn  10489  fz1sbc  10520  elfzp12  10523  fzm1  10524  fz01or  10535  fvinim0ffz  10677  suprzubdc  10688  zsupssdc  10690  xqltnle  10719  flqidz  10742  ceilqidz  10774  modqmuladdnn0  10826  frec2uzrand  10863  frecuzrdgtcl  10870  fzfig  10888  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  monoord  10943  seq3split  10946  seqsplitg  10947  iseqf1olemqval  10958  seq3id2  10984  seqhomog  10988  1exp  11026  bcval  11209  hashennn  11241  hashfibc  11305  zfz1isolem1  11314  zfz1iso  11315  seq3coll  11316  iswrdiz  11333  0wrd0  11352  lswlgt0cl  11379  ccatval1  11387  ccatval2  11388  ccatalpha  11403  ccatrcl1  11404  wrdl1s1  11420  ccats1val2  11430  wrd2ind  11517  pfxccatin12lem3  11526  pfxccatid  11535  reuccatpfxs1lem  11540  shftlem  11603  shftfibg  11607  shftfib  11610  shftfn  11611  2shfti  11618  rexuz3  11778  sqrt0rlem  11791  cau3  11904  negfi  12017  sumdc  12149  sumrbdclem  12169  summodclem2a  12173  fisumss  12184  prodrbdclem  12363  prodmodclem2a  12368  fprodssdc  12382  fprodsplit1f  12426  ef0lem  12452  odd2np1  12665  even2n  12666  oddnn02np1  12672  oddge22np1  12673  evennn02n  12674  evennn2n  12675  nn0enne  12694  divalgmod  12719  uzwodc  12839  lcmgcdlem  12880  cncongr1  12906  1nprm  12917  isprm2  12920  dvdsnprmd  12928  prmdc  12933  exprmfct  12942  nprmdvds1  12944  coprm  12948  prmdiveq  13043  prm23lt5  13071  pcpre1  13100  pc2dvds  13138  pcz  13140  pcmpt  13151  qexpz  13160  4sqlem2  13197  4sqlem19  13217  prmlem0  13249  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ennnfonelemhom  13364  ctiunctlemudc  13386  ssnnctlemct  13395  nninfdclemcl  13397  imasaddfnlemg  13694  ismgmid  13756  isgrpid2  13904  mhmlem  13976  eqgval  14085  dvdsrcl2  14515  nzrunit  14604  lringuplu  14612  dvdsrzring  15047  znrrg  15104  mplsubgfilemm  15214  fiinopn  15230  istopon  15239  basis2  15274  eltg3  15283  tg2  15286  tgidm  15300  bastop  15301  bastop2  15310  topnex  15312  isopn3  15351  tgrest  15395  cnpval  15424  lmbr  15439  cnconst  15460  txbas  15484  uptx  15500  txdis1cn  15504  cnmpt12  15513  cnmpt22  15520  hmeocnvb  15544  xblm  15643  isxms2  15678  mopni  15708  blssioo  15779  dedekindeulemuub  15843  dedekindeulemeu  15848  dedekindicclemuub  15852  dedekindicclemeu  15857  ivthinclemlm  15860  ivthinclemum  15861  ivthreinc  15871  pellexlem3  16231  bposlem5  16315  lgsfvalg  16329  lgsval2lem  16334  lgsdir2lem2  16353  gausslemma2dlem1a  16382  gausslemma2dlem4  16388  gausslemma2dlem6  16391  2lgslem1b  16413  2lgs  16428  2lgsoddprmlem2  16430  2lgsoddprmlem3  16435  2sqlem2  16439  2sqlem6  16444  2sqlem7  16445  2sqlem10  16449  vtxvalg  16462  iedgvalg  16463  umgredg  16591  upgrpredgv  16592  usgredg2vlem2  16669  ushgredgedg  16672  ushgredgedgloop  16674  griedg0ssusgr  16697  uhgrspansubgrlem  16722  vtxdgfifival  16737  iswlk  16769  upgrwlkvtxedg  16810  isclwwlknx  16862  clwwlkn1loopb  16866  clwwlknonex2lem1  16883  elabgf0  17010  bj-rspgt  17019  cbvrald  17021  decidi  17028  sumdc2  17032  bdssex  17133  bj-inex  17138  bj-intnexr  17140  bj-unexg  17152  bj-d0clsepcl  17156  bj-nnelirr  17184  bj-nn0suc  17195  bj-inf2vnlem1  17201  bj-inf2vnlem2  17202  bj-inf2vnlem3  17203  bj-inf2vnlem4  17204  bj-nn0sucALT  17209  bj-findis  17210  3dom  17223  wexmiddiffilem  17248  wexmiddifxy  17251  trilpolemcl  17293