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  4108  cbvmpt  4139  trel  4149  trss  4151  ssex  4181  intnexr  4195  intexabim  4196  exmidel  4249  euabex  4269  elopab  4304  opelopab2a  4311  frirrg  4397  tz7.2  4401  ordelord  4428  onm  4448  ralxfr2d  4511  rexxfr2d  4512  rabxfrd  4516  reuhypd  4518  ordtriexmid  4569  ontriexmidim  4570  ordtri2orexmid  4571  ontr2exmid  4573  onsucsssucexmid  4575  onsucelsucexmid  4578  ordsucunielexmid  4579  regexmidlem1  4581  elirr  4589  nordeq  4592  sucprcreg  4597  en2lp  4602  ordsoexmid  4610  ordsuc  4611  onsucuni2  4612  tfis  4631  peano2  4643  findes  4651  limom  4662  opelxp  4705  opeliunxp  4730  opbrop  4754  ssrel  4763  ssrel2  4765  ssrelrel  4775  relopabi  4803  eliunxp  4817  opeliunxp2  4818  ideqg  4829  dmmrnm  4897  dmxpm  4898  elreldm  4904  elrnmptg  4930  elres  4995  resiexg  5004  dfres2  5011  imai  5038  elimasng  5050  issref  5065  xpmlem  5103  xpm  5104  elxp4  5170  elxp5  5171  unielrel  5210  relcnvexb  5222  dmfex  5465  funfveu  5589  funimass4  5629  fvelimab  5635  ssimaex  5640  fvopab3g  5652  fvopab3ig  5653  fvmptssdm  5664  chfnrn  5691  fvelrn  5711  fmpt  5730  ffnfv  5738  fmptco  5746  elunirn  5835  f1elima  5842  cbvriota  5910  acexmidlemab  5938  acexmidlemcase  5939  cbvmpox  6023  eloprabga  6032  resoprab  6041  elrnmpo  6059  ov  6065  ovig  6067  ov6g  6084  ovg  6085  ovelrn  6095  caovimo  6140  fo1stresm  6247  fo2ndresm  6248  elxp6  6255  unielxp  6260  eqop2  6264  dfoprab4  6278  dfoprab4f  6279  fmpox  6286  1stconst  6307  2ndconst  6308  f1o2ndf1  6314  xporderlem  6317  f1od2  6321  disjxp1  6322  opeliunxp2f  6324  dftpos3  6348  dftpos4  6349  tpostpos  6350  smoel  6386  tfr1onlemaccex  6434  tfrcllemaccex  6447  tfrcl  6450  frecabcl  6485  frecsuc  6493  nntri3or  6579  nntri3  6583  nndcel  6586  riinerm  6695  th3qlem1  6724  mapsncnv  6782  elixpsn  6822  dom2lem  6863  fiprc  6907  xpsnen  6916  phplem3g  6953  phpelm  6963  ssfiexmid  6973  domfiexmid  6975  inffiexmid  7003  undifdcss  7020  opabfi  7035  snon0  7037  f1dmvrnfibi  7046  f1vrnfibi  7047  ordiso2  7137  ctssdclemn0  7212  ctssdc  7215  enumct  7217  nnnninf  7228  nnnninfeq  7230  nninfisollemne  7233  nninfisol  7235  finomni  7242  exmidlpo  7245  acneq  7314  finacn  7316  acfun  7319  exmidontriimlem3  7335  exmidontriimlem4  7336  pw1ne1  7341  onntri35  7349  exmidapne  7372  ccfunen  7376  cc2lem  7378  elni2  7427  recexnq  7503  recmulnqg  7504  enq0enq  7544  enq0sym  7545  enq0ref  7546  enq0tr  7547  enq0breq  7549  nqnq0pi  7551  nqnq0  7554  prop  7588  prcdnql  7597  prcunqu  7598  prubl  7599  prltlu  7600  prnmaxl  7601  prnminu  7602  prdisj  7605  prarloc  7616  genipv  7622  genpelvl  7625  genpelvu  7626  genprndl  7634  genprndu  7635  distrlem5prl  7699  distrlem5pru  7700  ltexprlemm  7713  ltexprlemdisj  7719  ltexprlemloc  7720  ltexprlemrl  7723  ltexprlemru  7725  aptiprleml  7752  aptiprlemu  7753  archpr  7756  cauappcvgprlemm  7758  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  caucvgprlemm  7781  caucvgprlemladdfu  7790  caucvgprprlemmu  7808  elreal2  7943  ltresr  7952  axcnre  7994  axpre-suploclemres  8014  0re  8072  renepnf  8120  renemnf  8121  ltxrlt  8138  eqlei2  8167  0cnALT  8262  sup3exmid  9030  nn1suc  9055  nnne0  9064  xnn0xr  9363  nn0nepnf  9366  elz  9374  elnn0z  9385  elz2  9444  uzind4s  9711  elnn1uz2  9728  qre  9746  elpqb  9771  xnn0lenn0nn0  9987  xsubge0  10003  xposdif  10004  xleaddadd  10009  fzsn  10188  fz1sbc  10218  elfzp12  10221  fzm1  10222  fz01or  10233  fvinim0ffz  10370  suprzubdc  10379  zsupssdc  10381  xqltnle  10410  flqidz  10429  ceilqidz  10461  modqmuladdnn0  10513  frec2uzrand  10550  frecuzrdgtcl  10557  fzfig  10575  seq3fveq2  10620  seqfveq2g  10622  seq3shft2  10626  seqshft2g  10627  monoord  10630  seq3split  10633  seqsplitg  10634  iseqf1olemqval  10645  seq3id2  10671  seqhomog  10675  1exp  10713  bcval  10894  hashennn  10925  zfz1isolem1  10985  zfz1iso  10986  seq3coll  10987  iswrdiz  11001  0wrd0  11020  lswlgt0cl  11045  ccatval1  11053  ccatval2  11054  wrdl1s1  11084  ccats1val2  11092  shftlem  11127  shftfibg  11131  shftfib  11134  shftfn  11135  2shfti  11142  rexuz3  11301  sqrt0rlem  11314  cau3  11426  negfi  11539  sumdc  11669  sumrbdclem  11688  summodclem2a  11692  fisumss  11703  prodrbdclem  11882  prodmodclem2a  11887  fprodssdc  11901  fprodsplit1f  11945  ef0lem  11971  odd2np1  12184  even2n  12185  oddnn02np1  12191  oddge22np1  12192  evennn02n  12193  evennn2n  12194  nn0enne  12213  divalgmod  12238  uzwodc  12358  lcmgcdlem  12399  cncongr1  12425  1nprm  12436  isprm2  12439  dvdsnprmd  12447  prmdc  12452  exprmfct  12460  nprmdvds1  12462  coprm  12466  prmdiveq  12558  prm23lt5  12586  pcpre1  12615  pc2dvds  12653  pcz  12655  pcmpt  12666  qexpz  12675  4sqlem2  12712  4sqlem19  12732  ennnfonelemhom  12786  ctiunctlemudc  12808  ssnnctlemct  12817  nninfdclemcl  12819  imasaddfnlemg  13146  ismgmid  13209  isgrpid2  13372  mhmlem  13450  eqgval  13559  dvdsrcl2  13861  nzrunit  13950  lringuplu  13958  dvdsrzring  14365  znrrg  14422  mplsubgfilemm  14460  fiinopn  14476  istopon  14485  basis2  14520  eltg3  14529  tg2  14532  tgidm  14546  bastop  14547  bastop2  14556  topnex  14558  isopn3  14597  tgrest  14641  cnpval  14670  lmbr  14685  cnconst  14706  txbas  14730  uptx  14746  txdis1cn  14750  cnmpt12  14759  cnmpt22  14766  hmeocnvb  14790  xblm  14889  isxms2  14924  mopni  14954  blssioo  15025  dedekindeulemuub  15089  dedekindeulemeu  15094  dedekindicclemuub  15098  dedekindicclemeu  15103  ivthinclemlm  15106  ivthinclemum  15107  ivthreinc  15117  lgsfvalg  15482  lgsval2lem  15487  lgsdir2lem2  15506  gausslemma2dlem1a  15535  gausslemma2dlem4  15541  gausslemma2dlem6  15544  2lgslem1b  15566  2lgs  15581  2lgsoddprmlem2  15583  2lgsoddprmlem3  15588  2sqlem2  15592  2sqlem6  15597  2sqlem7  15598  2sqlem10  15602  vtxvalg  15615  iedgvalg  15616  elabgf0  15713  bj-rspgt  15722  cbvrald  15724  decidi  15731  sumdc2  15735  bdssex  15838  bj-inex  15843  bj-intnexr  15845  bj-unexg  15857  bj-d0clsepcl  15861  bj-nnelirr  15889  bj-nn0suc  15900  bj-inf2vnlem1  15906  bj-inf2vnlem2  15907  bj-inf2vnlem3  15908  bj-inf2vnlem4  15909  bj-nn0sucALT  15914  bj-findis  15915  trilpolemcl  15976