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  4195  cbvmpt  4226  trel  4236  trss  4238  ssex  4270  intnexr  4287  intexabim  4288  exmidel  4342  euabex  4365  elopab  4400  opelopab2a  4407  frirrg  4495  tz7.2  4499  ordelord  4526  onm  4546  ralxfr2d  4610  rexxfr2d  4611  rabxfrd  4615  reuhypd  4617  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  ordsucunielexmid  4678  regexmidlem1  4680  elirr  4688  nordeq  4691  sucprcreg  4696  en2lp  4701  ordsoexmid  4709  ordsuc  4710  onsucuni2  4711  tfis  4730  peano2  4742  findes  4750  limom  4761  opelxp  4804  opeliunxp  4830  opbrop  4854  ssrel  4863  ssrel2  4865  ssrelrel  4875  relopabi  4905  eliunxp  4919  opeliunxp2  4920  ideqg  4931  reldmm  5000  dmmrnm  5001  dmxpm  5002  elreldm  5008  elrnmptg  5034  elres  5099  resiexg  5108  dfres2  5115  imai  5143  elimasng  5155  issref  5170  xpmlem  5208  xpm  5209  elxp4  5275  elxp5  5276  unielrel  5315  relcnvexb  5327  dmfex  5582  funfveu  5708  funimass4  5753  fvelimab  5759  ssimaex  5764  fvopab3g  5778  fvopab3ig  5779  fvmptssdm  5790  chfnrn  5820  fvelrn  5839  fmpt  5858  ffnfv  5866  fmptco  5874  elunirn  5972  f1elima  5979  cbvriota  6050  acexmidlemab  6079  acexmidlemcase  6080  cbvmpox  6166  eloprabga  6175  resoprab  6184  elrnmpo  6202  ov  6208  ovig  6210  ov6g  6227  ovg  6228  ovelrn  6238  caovimo  6283  abrexss  6358  fo1stresm  6395  fo2ndresm  6396  elxp6  6403  unielxp  6408  eqop2  6412  dfoprab4  6426  dfoprab4f  6427  fmpox  6436  1stconst  6457  2ndconst  6458  f1o2ndf1  6464  xporderlem  6467  f1od2  6471  disjxp1  6472  opeliunxp2f  6509  dftpos3  6533  dftpos4  6534  tpostpos  6535  smoel  6571  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcl  6635  frecabcl  6670  frecsuc  6678  nntri3or  6766  nntri3  6770  nndcel  6773  riinerm  6882  th3qlem1  6911  mapsncnv  6977  elixpsn  7017  dom2lem  7058  fiprc  7104  xpsnen  7119  phplem3g  7157  phpelm  7168  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  elssdc  7209  inffiexmid  7213  undifdcss  7230  opabfi  7247  snon0  7249  f1dmvrnfibi  7258  f1vrnfibi  7259  suppeqfsuppbi  7295  ordiso2  7375  ctssdclemn0  7450  ctssdc  7453  enumct  7455  nnnninf  7466  nnnninfeq  7468  nninfisollemne  7471  nninfisol  7473  finomni  7480  exmidlpo  7483  pr2cv1  7541  acneq  7558  finacn  7560  acfun  7563  exmidontriimlem3  7579  exmidontriimlem4  7580  pw1ne1  7588  onntri35  7596  exmidapne  7626  ccfunen  7630  cc2lem  7632  elni2  7681  recexnq  7757  recmulnqg  7758  enq0enq  7798  enq0sym  7799  enq0ref  7800  enq0tr  7801  enq0breq  7803  nqnq0pi  7805  nqnq0  7808  prop  7842  prcdnql  7851  prcunqu  7852  prubl  7853  prltlu  7854  prnmaxl  7855  prnminu  7856  prdisj  7859  prarloc  7870  genipv  7876  genpelvl  7879  genpelvu  7880  genprndl  7888  genprndu  7889  distrlem5prl  7953  distrlem5pru  7954  ltexprlemm  7967  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  aptiprleml  8006  aptiprlemu  8007  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  caucvgprlemm  8035  caucvgprlemladdfu  8044  caucvgprprlemmu  8062  elreal2  8197  ltresr  8206  axcnre  8248  axpre-suploclemres  8268  0re  8326  renepnf  8373  renemnf  8374  ltxrlt  8391  eqlei2  8420  0cnALT  8516  sup3exmid  9287  nn1suc  9323  nnne0  9332  xnn0xr  9635  nn0nepnf  9638  elz  9646  elnn0z  9657  elz2  9716  uzind4s  9990  elnn1uz2  10007  qre  10025  elpqb  10050  xnn0lenn0nn0  10267  xsubge0  10283  xposdif  10284  xleaddadd  10289  fzsn  10472  fz1sbc  10503  elfzp12  10506  fzm1  10507  fz01or  10518  fvinim0ffz  10660  suprzubdc  10671  zsupssdc  10673  xqltnle  10702  flqidz  10721  ceilqidz  10753  modqmuladdnn0  10805  frec2uzrand  10842  frecuzrdgtcl  10849  fzfig  10867  seq3fveq2  10912  seqfveq2g  10914  seq3shft2  10918  seqshft2g  10919  monoord  10922  seq3split  10925  seqsplitg  10926  iseqf1olemqval  10937  seq3id2  10963  seqhomog  10967  1exp  11005  bcval  11187  hashennn  11219  hashfibc  11283  zfz1isolem1  11292  zfz1iso  11293  seq3coll  11294  iswrdiz  11311  0wrd0  11330  lswlgt0cl  11357  ccatval1  11365  ccatval2  11366  ccatalpha  11381  ccatrcl1  11382  wrdl1s1  11398  ccats1val2  11408  wrd2ind  11495  pfxccatin12lem3  11504  pfxccatid  11513  reuccatpfxs1lem  11518  shftlem  11581  shftfibg  11585  shftfib  11588  shftfn  11589  2shfti  11596  rexuz3  11756  sqrt0rlem  11769  cau3  11881  negfi  11994  sumdc  12124  sumrbdclem  12144  summodclem2a  12148  fisumss  12159  prodrbdclem  12338  prodmodclem2a  12343  fprodssdc  12357  fprodsplit1f  12401  ef0lem  12427  odd2np1  12640  even2n  12641  oddnn02np1  12647  oddge22np1  12648  evennn02n  12649  evennn2n  12650  nn0enne  12669  divalgmod  12694  uzwodc  12814  lcmgcdlem  12855  cncongr1  12881  1nprm  12892  isprm2  12895  dvdsnprmd  12903  prmdc  12908  exprmfct  12916  nprmdvds1  12918  coprm  12922  prmdiveq  13014  prm23lt5  13042  pcpre1  13071  pc2dvds  13109  pcz  13111  pcmpt  13122  qexpz  13131  4sqlem2  13168  4sqlem19  13188  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ennnfonelemhom  13306  ctiunctlemudc  13328  ssnnctlemct  13337  nninfdclemcl  13339  imasaddfnlemg  13635  ismgmid  13697  isgrpid2  13845  mhmlem  13917  eqgval  14026  dvdsrcl2  14406  nzrunit  14495  lringuplu  14503  dvdsrzring  14938  znrrg  14995  mplsubgfilemm  15089  fiinopn  15105  istopon  15114  basis2  15149  eltg3  15158  tg2  15161  tgidm  15175  bastop  15176  bastop2  15185  topnex  15187  isopn3  15226  tgrest  15270  cnpval  15299  lmbr  15314  cnconst  15335  txbas  15359  uptx  15375  txdis1cn  15379  cnmpt12  15388  cnmpt22  15395  hmeocnvb  15419  xblm  15518  isxms2  15553  mopni  15583  blssioo  15654  dedekindeulemuub  15718  dedekindeulemeu  15723  dedekindicclemuub  15727  dedekindicclemeu  15732  ivthinclemlm  15735  ivthinclemum  15736  ivthreinc  15746  pellexlem3  16093  lgsfvalg  16124  lgsval2lem  16129  lgsdir2lem2  16148  gausslemma2dlem1a  16177  gausslemma2dlem4  16183  gausslemma2dlem6  16186  2lgslem1b  16208  2lgs  16223  2lgsoddprmlem2  16225  2lgsoddprmlem3  16230  2sqlem2  16234  2sqlem6  16239  2sqlem7  16240  2sqlem10  16244  vtxvalg  16257  iedgvalg  16258  umgredg  16386  upgrpredgv  16387  usgredg2vlem2  16464  ushgredgedg  16467  ushgredgedgloop  16469  griedg0ssusgr  16492  uhgrspansubgrlem  16517  vtxdgfifival  16532  iswlk  16564  upgrwlkvtxedg  16605  isclwwlknx  16657  clwwlkn1loopb  16661  clwwlknonex2lem1  16678  elabgf0  16805  bj-rspgt  16814  cbvrald  16816  decidi  16823  sumdc2  16827  bdssex  16928  bj-inex  16933  bj-intnexr  16935  bj-unexg  16947  bj-d0clsepcl  16951  bj-nnelirr  16979  bj-nn0suc  16990  bj-inf2vnlem1  16996  bj-inf2vnlem2  16997  bj-inf2vnlem3  16998  bj-inf2vnlem4  16999  bj-nn0sucALT  17004  bj-findis  17005  3dom  17018  wexmiddiffilem  17043  wexmiddifxy  17046  trilpolemcl  17086