Theorem eleq1 2268

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 2215	. . . 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 1848	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2201	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2201	. 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 1373   E.wex 1515   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleq12  2270  eleq1i  2271  eleq1d  2274  eleq1a  2277  cleqh  2305  nelneq  2306  clelsb1  2310  nfcjust  2336  cleqf  2373  nelne2  2467  neleq1  2475  rgen2a  2560  cbvralf  2730  cbvrexf  2731  cbvreu  2736  cbvrab  2770  eqvisset  2782  ceqsralt  2799  vtoclgaf  2838  vtocl2gaf  2840  vtocl3gaf  2842  rspct  2870  rspc  2871  rspce  2872  rspc2gv  2889  ceqsrexv  2903  ceqsrexbv  2904  clel2  2906  elabgt  2914  elabgf  2915  elrabi  2926  elrabf  2927  elrab3t  2928  ralab2  2937  rexab2  2939  mo2icl  2952  morex  2957  reu2  2961  reu6  2962  rmo4  2966  reu8  2969  reuind  2978  nelrdva  2980  ru  2997  dfsbcq  3000  dfsbcq2  3001  sbc8g  3006  sbcel1v  3061  rmob  3091  difjust  3167  unjust  3169  injust  3171  eldif  3175  dfss2f  3184  uniiunlem  3282  elun  3314  elin  3356  rabn0m  3488  disjne  3514  r19.3rm  3549  r19.9rmv  3552  raaanlem  3565  raaan  3566  ifmdc  3612  elpwg  3624  elpr2  3655  elsn2g  3666  rabsn  3700  tpid3g  3748  snssb  3766  snssgOLD  3769  difsn  3770  sssnm  3795  opeq1  3819  opeq2  3820  eluni  3853  elunii  3855  eluniab  3862  elint  3891  elintg  3893  elintab  3896  elintrabg  3898  intss1  3900  eliun  3931  eliin  3932  dfiunv2  3963  opabss  4109  cbvmpt  4140  trel  4150  trss  4152  ssex  4182  intnexr  4196  intexabim  4197  exmidel  4250  euabex  4270  elopab  4305  opelopab2a  4312  frirrg  4398  tz7.2  4402  ordelord  4429  onm  4449  ralxfr2d  4512  rexxfr2d  4513  rabxfrd  4517  reuhypd  4519  ordtriexmid  4570  ontriexmidim  4571  ordtri2orexmid  4572  ontr2exmid  4574  onsucsssucexmid  4576  onsucelsucexmid  4579  ordsucunielexmid  4580  regexmidlem1  4582  elirr  4590  nordeq  4593  sucprcreg  4598  en2lp  4603  ordsoexmid  4611  ordsuc  4612  onsucuni2  4613  tfis  4632  peano2  4644  findes  4652  limom  4663  opelxp  4706  opeliunxp  4731  opbrop  4755  ssrel  4764  ssrel2  4766  ssrelrel  4776  relopabi  4804  eliunxp  4818  opeliunxp2  4819  ideqg  4830  dmmrnm  4898  dmxpm  4899  elreldm  4905  elrnmptg  4931  elres  4996  resiexg  5005  dfres2  5012  imai  5039  elimasng  5051  issref  5066  xpmlem  5104  xpm  5105  elxp4  5171  elxp5  5172  unielrel  5211  relcnvexb  5223  dmfex  5467  funfveu  5591  funimass4  5631  fvelimab  5637  ssimaex  5642  fvopab3g  5654  fvopab3ig  5655  fvmptssdm  5666  chfnrn  5693  fvelrn  5713  fmpt  5732  ffnfv  5740  fmptco  5748  elunirn  5837  f1elima  5844  cbvriota  5912  acexmidlemab  5940  acexmidlemcase  5941  cbvmpox  6025  eloprabga  6034  resoprab  6043  elrnmpo  6061  ov  6067  ovig  6069  ov6g  6086  ovg  6087  ovelrn  6097  caovimo  6142  fo1stresm  6249  fo2ndresm  6250  elxp6  6257  unielxp  6262  eqop2  6266  dfoprab4  6280  dfoprab4f  6281  fmpox  6288  1stconst  6309  2ndconst  6310  f1o2ndf1  6316  xporderlem  6319  f1od2  6323  disjxp1  6324  opeliunxp2f  6326  dftpos3  6350  dftpos4  6351  tpostpos  6352  smoel  6388  tfr1onlemaccex  6436  tfrcllemaccex  6449  tfrcl  6452  frecabcl  6487  frecsuc  6495  nntri3or  6581  nntri3  6585  nndcel  6588  riinerm  6697  th3qlem1  6726  mapsncnv  6784  elixpsn  6824  dom2lem  6865  fiprc  6909  xpsnen  6918  phplem3g  6955  phpelm  6965  ssfiexmid  6975  domfiexmid  6977  inffiexmid  7005  undifdcss  7022  opabfi  7037  snon0  7039  f1dmvrnfibi  7048  f1vrnfibi  7049  ordiso2  7139  ctssdclemn0  7214  ctssdc  7217  enumct  7219  nnnninf  7230  nnnninfeq  7232  nninfisollemne  7235  nninfisol  7237  finomni  7244  exmidlpo  7247  acneq  7316  finacn  7318  acfun  7321  exmidontriimlem3  7337  exmidontriimlem4  7338  pw1ne1  7343  onntri35  7351  exmidapne  7374  ccfunen  7378  cc2lem  7380  elni2  7429  recexnq  7505  recmulnqg  7506  enq0enq  7546  enq0sym  7547  enq0ref  7548  enq0tr  7549  enq0breq  7551  nqnq0pi  7553  nqnq0  7556  prop  7590  prcdnql  7599  prcunqu  7600  prubl  7601  prltlu  7602  prnmaxl  7603  prnminu  7604  prdisj  7607  prarloc  7618  genipv  7624  genpelvl  7627  genpelvu  7628  genprndl  7636  genprndu  7637  distrlem5prl  7701  distrlem5pru  7702  ltexprlemm  7715  ltexprlemdisj  7721  ltexprlemloc  7722  ltexprlemrl  7725  ltexprlemru  7727  aptiprleml  7754  aptiprlemu  7755  archpr  7758  cauappcvgprlemm  7760  cauappcvgprlemladdfu  7769  cauappcvgprlemladdfl  7770  caucvgprlemm  7783  caucvgprlemladdfu  7792  caucvgprprlemmu  7810  elreal2  7945  ltresr  7954  axcnre  7996  axpre-suploclemres  8016  0re  8074  renepnf  8122  renemnf  8123  ltxrlt  8140  eqlei2  8169  0cnALT  8264  sup3exmid  9032  nn1suc  9057  nnne0  9066  xnn0xr  9365  nn0nepnf  9368  elz  9376  elnn0z  9387  elz2  9446  uzind4s  9713  elnn1uz2  9730  qre  9748  elpqb  9773  xnn0lenn0nn0  9989  xsubge0  10005  xposdif  10006  xleaddadd  10011  fzsn  10190  fz1sbc  10220  elfzp12  10223  fzm1  10224  fz01or  10235  fvinim0ffz  10372  suprzubdc  10381  zsupssdc  10383  xqltnle  10412  flqidz  10431  ceilqidz  10463  modqmuladdnn0  10515  frec2uzrand  10552  frecuzrdgtcl  10559  fzfig  10577  seq3fveq2  10622  seqfveq2g  10624  seq3shft2  10628  seqshft2g  10629  monoord  10632  seq3split  10635  seqsplitg  10636  iseqf1olemqval  10647  seq3id2  10673  seqhomog  10677  1exp  10715  bcval  10896  hashennn  10927  zfz1isolem1  10987  zfz1iso  10988  seq3coll  10989  iswrdiz  11003  0wrd0  11022  lswlgt0cl  11048  ccatval1  11056  ccatval2  11057  wrdl1s1  11087  ccats1val2  11095  shftlem  11160  shftfibg  11164  shftfib  11167  shftfn  11168  2shfti  11175  rexuz3  11334  sqrt0rlem  11347  cau3  11459  negfi  11572  sumdc  11702  sumrbdclem  11721  summodclem2a  11725  fisumss  11736  prodrbdclem  11915  prodmodclem2a  11920  fprodssdc  11934  fprodsplit1f  11978  ef0lem  12004  odd2np1  12217  even2n  12218  oddnn02np1  12224  oddge22np1  12225  evennn02n  12226  evennn2n  12227  nn0enne  12246  divalgmod  12271  uzwodc  12391  lcmgcdlem  12432  cncongr1  12458  1nprm  12469  isprm2  12472  dvdsnprmd  12480  prmdc  12485  exprmfct  12493  nprmdvds1  12495  coprm  12499  prmdiveq  12591  prm23lt5  12619  pcpre1  12648  pc2dvds  12686  pcz  12688  pcmpt  12699  qexpz  12708  4sqlem2  12745  4sqlem19  12765  ennnfonelemhom  12819  ctiunctlemudc  12841  ssnnctlemct  12850  nninfdclemcl  12852  imasaddfnlemg  13179  ismgmid  13242  isgrpid2  13405  mhmlem  13483  eqgval  13592  dvdsrcl2  13894  nzrunit  13983  lringuplu  13991  dvdsrzring  14398  znrrg  14455  mplsubgfilemm  14493  fiinopn  14509  istopon  14518  basis2  14553  eltg3  14562  tg2  14565  tgidm  14579  bastop  14580  bastop2  14589  topnex  14591  isopn3  14630  tgrest  14674  cnpval  14703  lmbr  14718  cnconst  14739  txbas  14763  uptx  14779  txdis1cn  14783  cnmpt12  14792  cnmpt22  14799  hmeocnvb  14823  xblm  14922  isxms2  14957  mopni  14987  blssioo  15058  dedekindeulemuub  15122  dedekindeulemeu  15127  dedekindicclemuub  15131  dedekindicclemeu  15136  ivthinclemlm  15139  ivthinclemum  15140  ivthreinc  15150  lgsfvalg  15515  lgsval2lem  15520  lgsdir2lem2  15539  gausslemma2dlem1a  15568  gausslemma2dlem4  15574  gausslemma2dlem6  15577  2lgslem1b  15599  2lgs  15614  2lgsoddprmlem2  15616  2lgsoddprmlem3  15621  2sqlem2  15625  2sqlem6  15630  2sqlem7  15631  2sqlem10  15635  vtxvalg  15648  iedgvalg  15649  elabgf0  15750  bj-rspgt  15759  cbvrald  15761  decidi  15768  sumdc2  15772  bdssex  15875  bj-inex  15880  bj-intnexr  15882  bj-unexg  15894  bj-d0clsepcl  15898  bj-nnelirr  15926  bj-nn0suc  15937  bj-inf2vnlem1  15943  bj-inf2vnlem2  15944  bj-inf2vnlem3  15945  bj-inf2vnlem4  15946  bj-nn0sucALT  15951  bj-findis  15952  trilpolemcl  16013