Theorem eleq1 2270

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 2217	. . . 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 1849	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2203	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2203	. 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 1516   e. wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  eleq12  2272  eleq1i  2273  eleq1d  2276  eleq1a  2279  cleqh  2307  nelneq  2308  clelsb1  2312  nfcjust  2338  cleqf  2375  nelne2  2469  neleq1  2477  rgen2a  2562  cbvralf  2733  cbvrexf  2734  cbvreu  2740  cbvrab  2774  eqvisset  2787  ceqsralt  2804  vtoclgaf  2843  vtocl2gaf  2845  vtocl3gaf  2847  rspct  2877  rspc  2878  rspce  2879  rspc2gv  2896  ceqsrexv  2910  ceqsrexbv  2911  clel2  2913  elabgt  2921  elabgf  2922  elrabi  2933  elrabf  2934  elrab3t  2935  ralab2  2944  rexab2  2946  mo2icl  2959  morex  2964  reu2  2968  reu6  2969  rmo4  2973  reu8  2976  reuind  2985  nelrdva  2987  ru  3004  dfsbcq  3007  dfsbcq2  3008  sbc8g  3013  sbcel1v  3068  rmob  3099  difjust  3175  unjust  3177  injust  3179  eldif  3183  dfss2f  3192  uniiunlem  3290  elun  3322  elin  3364  rabn0m  3496  disjne  3522  r19.3rm  3557  r19.9rmv  3560  raaanlem  3573  raaan  3574  elif  3591  ifmdc  3622  elpwg  3634  elpr2  3665  elsn2g  3676  rabsn  3710  tpid3g  3758  snssb  3777  snssgOLD  3780  difsn  3781  sssnm  3808  opeq1  3833  opeq2  3834  eluni  3867  elunii  3869  eluniab  3876  elint  3905  elintg  3907  elintab  3910  elintrabg  3912  intss1  3914  eliun  3945  eliin  3946  dfiunv2  3977  opabss  4124  cbvmpt  4155  trel  4165  trss  4167  ssex  4197  intnexr  4211  intexabim  4212  exmidel  4265  euabex  4287  elopab  4322  opelopab2a  4329  frirrg  4415  tz7.2  4419  ordelord  4446  onm  4466  ralxfr2d  4529  rexxfr2d  4530  rabxfrd  4534  reuhypd  4536  ordtriexmid  4587  ontriexmidim  4588  ordtri2orexmid  4589  ontr2exmid  4591  onsucsssucexmid  4593  onsucelsucexmid  4596  ordsucunielexmid  4597  regexmidlem1  4599  elirr  4607  nordeq  4610  sucprcreg  4615  en2lp  4620  ordsoexmid  4628  ordsuc  4629  onsucuni2  4630  tfis  4649  peano2  4661  findes  4669  limom  4680  opelxp  4723  opeliunxp  4748  opbrop  4772  ssrel  4781  ssrel2  4783  ssrelrel  4793  relopabi  4821  eliunxp  4835  opeliunxp2  4836  ideqg  4847  dmmrnm  4916  dmxpm  4917  elreldm  4923  elrnmptg  4949  elres  5014  resiexg  5023  dfres2  5030  imai  5057  elimasng  5069  issref  5084  xpmlem  5122  xpm  5123  elxp4  5189  elxp5  5190  unielrel  5229  relcnvexb  5241  dmfex  5487  funfveu  5612  funimass4  5652  fvelimab  5658  ssimaex  5663  fvopab3g  5675  fvopab3ig  5676  fvmptssdm  5687  chfnrn  5714  fvelrn  5734  fmpt  5753  ffnfv  5761  fmptco  5769  elunirn  5858  f1elima  5865  cbvriota  5933  acexmidlemab  5961  acexmidlemcase  5962  cbvmpox  6046  eloprabga  6055  resoprab  6064  elrnmpo  6082  ov  6088  ovig  6090  ov6g  6107  ovg  6108  ovelrn  6118  caovimo  6163  fo1stresm  6270  fo2ndresm  6271  elxp6  6278  unielxp  6283  eqop2  6287  dfoprab4  6301  dfoprab4f  6302  fmpox  6309  1stconst  6330  2ndconst  6331  f1o2ndf1  6337  xporderlem  6340  f1od2  6344  disjxp1  6345  opeliunxp2f  6347  dftpos3  6371  dftpos4  6372  tpostpos  6373  smoel  6409  tfr1onlemaccex  6457  tfrcllemaccex  6470  tfrcl  6473  frecabcl  6508  frecsuc  6516  nntri3or  6602  nntri3  6606  nndcel  6609  riinerm  6718  th3qlem1  6747  mapsncnv  6805  elixpsn  6845  dom2lem  6886  fiprc  6931  xpsnen  6941  phplem3g  6978  phpelm  6989  ssfiexmid  6999  domfiexmid  7001  inffiexmid  7029  undifdcss  7046  opabfi  7061  snon0  7063  f1dmvrnfibi  7072  f1vrnfibi  7073  ordiso2  7163  ctssdclemn0  7238  ctssdc  7241  enumct  7243  nnnninf  7254  nnnninfeq  7256  nninfisollemne  7259  nninfisol  7261  finomni  7268  exmidlpo  7271  pr2cv1  7329  acneq  7345  finacn  7347  acfun  7350  exmidontriimlem3  7366  exmidontriimlem4  7367  pw1ne1  7375  onntri35  7383  exmidapne  7407  ccfunen  7411  cc2lem  7413  elni2  7462  recexnq  7538  recmulnqg  7539  enq0enq  7579  enq0sym  7580  enq0ref  7581  enq0tr  7582  enq0breq  7584  nqnq0pi  7586  nqnq0  7589  prop  7623  prcdnql  7632  prcunqu  7633  prubl  7634  prltlu  7635  prnmaxl  7636  prnminu  7637  prdisj  7640  prarloc  7651  genipv  7657  genpelvl  7660  genpelvu  7661  genprndl  7669  genprndu  7670  distrlem5prl  7734  distrlem5pru  7735  ltexprlemm  7748  ltexprlemdisj  7754  ltexprlemloc  7755  ltexprlemrl  7758  ltexprlemru  7760  aptiprleml  7787  aptiprlemu  7788  archpr  7791  cauappcvgprlemm  7793  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  caucvgprlemm  7816  caucvgprlemladdfu  7825  caucvgprprlemmu  7843  elreal2  7978  ltresr  7987  axcnre  8029  axpre-suploclemres  8049  0re  8107  renepnf  8155  renemnf  8156  ltxrlt  8173  eqlei2  8202  0cnALT  8297  sup3exmid  9065  nn1suc  9090  nnne0  9099  xnn0xr  9398  nn0nepnf  9401  elz  9409  elnn0z  9420  elz2  9479  uzind4s  9746  elnn1uz2  9763  qre  9781  elpqb  9806  xnn0lenn0nn0  10022  xsubge0  10038  xposdif  10039  xleaddadd  10044  fzsn  10223  fz1sbc  10253  elfzp12  10256  fzm1  10257  fz01or  10268  fvinim0ffz  10407  suprzubdc  10416  zsupssdc  10418  xqltnle  10447  flqidz  10466  ceilqidz  10498  modqmuladdnn0  10550  frec2uzrand  10587  frecuzrdgtcl  10594  fzfig  10612  seq3fveq2  10657  seqfveq2g  10659  seq3shft2  10663  seqshft2g  10664  monoord  10667  seq3split  10670  seqsplitg  10671  iseqf1olemqval  10682  seq3id2  10708  seqhomog  10712  1exp  10750  bcval  10931  hashennn  10962  zfz1isolem1  11022  zfz1iso  11023  seq3coll  11024  iswrdiz  11038  0wrd0  11057  lswlgt0cl  11083  ccatval1  11091  ccatval2  11092  wrdl1s1  11122  ccats1val2  11130  wrd2ind  11214  pfxccatin12lem3  11223  pfxccatid  11232  reuccatpfxs1lem  11237  shftlem  11242  shftfibg  11246  shftfib  11249  shftfn  11250  2shfti  11257  rexuz3  11416  sqrt0rlem  11429  cau3  11541  negfi  11654  sumdc  11784  sumrbdclem  11803  summodclem2a  11807  fisumss  11818  prodrbdclem  11997  prodmodclem2a  12002  fprodssdc  12016  fprodsplit1f  12060  ef0lem  12086  odd2np1  12299  even2n  12300  oddnn02np1  12306  oddge22np1  12307  evennn02n  12308  evennn2n  12309  nn0enne  12328  divalgmod  12353  uzwodc  12473  lcmgcdlem  12514  cncongr1  12540  1nprm  12551  isprm2  12554  dvdsnprmd  12562  prmdc  12567  exprmfct  12575  nprmdvds1  12577  coprm  12581  prmdiveq  12673  prm23lt5  12701  pcpre1  12730  pc2dvds  12768  pcz  12770  pcmpt  12781  qexpz  12790  4sqlem2  12827  4sqlem19  12847  ennnfonelemhom  12901  ctiunctlemudc  12923  ssnnctlemct  12932  nninfdclemcl  12934  imasaddfnlemg  13261  ismgmid  13324  isgrpid2  13487  mhmlem  13565  eqgval  13674  dvdsrcl2  13976  nzrunit  14065  lringuplu  14073  dvdsrzring  14480  znrrg  14537  mplsubgfilemm  14575  fiinopn  14591  istopon  14600  basis2  14635  eltg3  14644  tg2  14647  tgidm  14661  bastop  14662  bastop2  14671  topnex  14673  isopn3  14712  tgrest  14756  cnpval  14785  lmbr  14800  cnconst  14821  txbas  14845  uptx  14861  txdis1cn  14865  cnmpt12  14874  cnmpt22  14881  hmeocnvb  14905  xblm  15004  isxms2  15039  mopni  15069  blssioo  15140  dedekindeulemuub  15204  dedekindeulemeu  15209  dedekindicclemuub  15213  dedekindicclemeu  15218  ivthinclemlm  15221  ivthinclemum  15222  ivthreinc  15232  lgsfvalg  15597  lgsval2lem  15602  lgsdir2lem2  15621  gausslemma2dlem1a  15650  gausslemma2dlem4  15656  gausslemma2dlem6  15659  2lgslem1b  15681  2lgs  15696  2lgsoddprmlem2  15698  2lgsoddprmlem3  15703  2sqlem2  15707  2sqlem6  15712  2sqlem7  15713  2sqlem10  15717  vtxvalg  15730  iedgvalg  15731  umgredg  15849  upgrpredgv  15850  elabgf0  15913  bj-rspgt  15922  cbvrald  15924  decidi  15931  sumdc2  15935  bdssex  16037  bj-inex  16042  bj-intnexr  16044  bj-unexg  16056  bj-d0clsepcl  16060  bj-nnelirr  16088  bj-nn0suc  16099  bj-inf2vnlem1  16105  bj-inf2vnlem2  16106  bj-inf2vnlem3  16107  bj-inf2vnlem4  16108  bj-nn0sucALT  16113  bj-findis  16114  trilpolemcl  16178