Theorem eleq2 2298

Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eleq2	|- ( A = B -> ( C e. A <-> C e. B ) )

Proof of Theorem eleq2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2228	. . . . . 6 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
2	1	biimpi 120	. . . . 5 |- ( A = B -> A. x ( x e. A <-> x e. B ) )
3	2	19.21bi 1607	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
4	3	anbi2d 464	. . 3 |- ( A = B -> ( ( x = C /\ x e. A ) <-> ( x = C /\ x e. B ) ) )
5	4	exbidv 1874	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2230	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2230	. 2 |- ( C e. B <-> E. x ( x = C /\ x e. B ) )
8	5, 6, 7	3bitr4g 223	1 |- ( A = B -> ( C e. A <-> C e. B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1396   = wceq 1398   E.wex 1541   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eleq12  2299  eleq2i  2301  eleq2d  2304  nelneq2  2336  clelsb2  2340  dvelimdc  2407  nelne1  2504  neleq2  2514  raleqf  2739  rexeqf  2740  reueq1f  2741  rmoeq1f  2742  rabeqf  2805  clel3g  2954  clel4  2956  sbcbi2  3096  sbcel2gv  3109  csbeq2  3165  sbnfc2  3202  difeq2  3335  uneq1  3370  ineq1  3419  nel02  3517  n0i  3518  disjel  3568  exsnrex  3737  sneqr  3870  preqr1g  3876  preqr1  3878  preq12b  3880  prel12  3881  elunii  3925  eluniab  3932  ssuni  3942  elinti  3964  elintab  3966  intss1  3970  intmin  3975  intab  3984  iineq2  4014  dfiin2g  4030  breq  4117  axsep2  4235  zfauscl  4236  inuni  4273  exmidexmid  4315  ss1o0el1  4316  exmid01  4317  exmidundif  4325  exmidundifim  4326  rext  4337  intid  4346  mss  4348  opth1  4358  opeqex  4372  frforeq3  4474  frirrg  4477  limeq  4504  nsuceq0g  4545  suctr  4548  snnex  4576  uniuni  4579  iunpw  4608  ordtriexmidlem  4648  ordtriexmidlem2  4649  ordtriexmid  4650  ontriexmidim  4651  ordtri2orexmid  4652  ontr2exmid  4654  ordtri2or2exmidlem  4655  onsucelsucexmidlem  4658  onsucelsucexmid  4659  ordsucunielexmid  4660  regexmidlem1  4662  reg2exmidlema  4663  regexmid  4664  reg2exmid  4665  elirr  4670  en2lp  4683  suc11g  4686  dtruex  4688  ordsoexmid  4691  nlimsucg  4695  onintexmid  4702  reg3exmidlemwe  4708  reg3exmid  4709  peano5  4727  limom  4743  0elnn  4748  nn0eln0  4749  nnregexmid  4750  xpeq1  4770  xpeq2  4771  opthprc  4808  xp11m  5208  funopg  5393  dffo4  5832  funopdmsn  5871  elunirn  5947  f1oiso  6007  canth  6011  eusvobj2  6046  acexmidlema  6051  acexmidlemb  6052  acexmidlemab  6054  acexmidlem2  6057  mpoeq123  6122  oprssdmm  6380  unielxp  6383  cnvf1o  6436  smoel  6546  tfr0dm  6568  frecabcl  6645  nnsucelsuc  6739  nntri3or  6741  nntri2  6742  nntri3  6745  nndceq  6747  nnmordi  6764  nnaordex  6776  elqsn0m  6852  qsel  6861  mapsnd  6938  mapsn  6940  en2m  7081  pw2f1odclem  7102  findcard2s  7162  elssdc  7177  eqsndc  7178  undifdcss  7198  fissfi  7231  2omap  7284  ctssdclemr  7418  nnnninf2  7433  exmidonfinlem  7511  exmidfodomrlemr  7520  exmidfodomrlemrALT  7521  finacn  7526  exmidaclem  7530  exmidontriimlem3  7545  exmidontriimlem4  7546  exmidontriim  7547  iftrueb01  7548  pw1ne3  7555  sucpw1ne3  7557  sucpw1nel3  7558  onntri35  7562  acnccim  7604  elni2  7647  addnidpig  7669  elinp  7807  suplocexprlemdisj  8053  suplocexprlemub  8056  pitonn  8181  peano1nnnn  8185  peano2nnnn  8186  peano5nnnn  8225  sup3exmid  9253  peano5nni  9262  1nn  9270  peano2nn  9271  dfuzi  9711  uz11  9900  elfzonlteqm1  10582  frec2uzltd  10794  0tonninf  10831  1tonninf  10832  hashfibclem  11236  wrdsymb0  11287  lsw0  11302  swrdwrdsymbg  11386  sumeq1  12071  prodeq1f  12269  nninfctlemfo  12767  ballotfilemcdc  13173  ballotfilem7  13229  ctiunct  13281  ssomct  13286  issubm  13733  isnsg  13961  releqgg  13979  eqgex  13980  resghm  14019  ghmeql  14026  issubrg  14473  lmodfopnelem2  14605  islssm  14637  islssmg  14638  lspsneq0  14706  istopg  14996  fiinbas  15046  topbas  15064  epttop  15087  restbasg  15165  icnpimaex  15208  lmcvg  15214  iscnp4  15215  cncnpi  15225  cnconst2  15230  cnptoprest  15236  cnptoprest2  15237  cnpdis  15239  lmss  15243  lmff  15246  txbas  15255  eltx  15256  txcnp  15268  txlm  15276  blssps  15424  blss  15425  blssexps  15426  blssex  15427  neibl  15488  metss  15491  metrest  15503  xmettx  15507  metcnp3  15508  tgioo  15551  tgqioo  15552  uhgrm  16205  lpvtx  16206  incistruhgr  16217  umgrnloopv  16241  uhgredgm  16263  uhgrvtxedgiedgb  16270  upgredg2vtx  16275  uhgr2edg  16333  umgrvad2edg  16338  usgredg4  16342  uspgredg2vlem  16347  ushgredgedg  16353  subgruhgredgdm  16397  vtxd0nedgbfi  16426  1loopgrvd2fi  16432  wlk1walkdom  16486  bdsep2  16798  bdzfauscl  16802  bj-indeq  16841  bj-nn0suc0  16862  bj-nnelirr  16865  bj-peano4  16867  bj-inf2vnlem2  16883  bj-nn0sucALT  16890  bj-findis  16891  strcollnft  16896  sscoll2  16900  nninfsellemdc  16930  nninfsellemqall  16935  nnnninfex  16942