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  2953  clel4  2955  sbcbi2  3095  sbcel2gv  3108  csbeq2  3164  sbnfc2  3201  difeq2  3333  uneq1  3368  ineq1  3417  nel02  3515  n0i  3516  disjel  3565  exsnrex  3733  sneqr  3866  preqr1g  3872  preqr1  3874  preq12b  3876  prel12  3877  elunii  3921  eluniab  3928  ssuni  3938  elinti  3960  elintab  3962  intss1  3966  intmin  3971  intab  3980  iineq2  4010  dfiin2g  4026  breq  4113  axsep2  4231  zfauscl  4232  inuni  4269  exmidexmid  4311  ss1o0el1  4312  exmid01  4313  exmidundif  4321  exmidundifim  4322  rext  4333  intid  4342  mss  4344  opth1  4354  opeqex  4368  frforeq3  4470  frirrg  4473  limeq  4500  nsuceq0g  4541  suctr  4544  snnex  4571  uniuni  4574  iunpw  4603  ordtriexmidlem  4643  ordtriexmidlem2  4644  ordtriexmid  4645  ontriexmidim  4646  ordtri2orexmid  4647  ontr2exmid  4649  ordtri2or2exmidlem  4650  onsucelsucexmidlem  4653  onsucelsucexmid  4654  ordsucunielexmid  4655  regexmidlem1  4657  reg2exmidlema  4658  regexmid  4659  reg2exmid  4660  elirr  4665  en2lp  4678  suc11g  4681  dtruex  4683  ordsoexmid  4686  nlimsucg  4690  onintexmid  4697  reg3exmidlemwe  4703  reg3exmid  4704  peano5  4722  limom  4738  0elnn  4743  nn0eln0  4744  nnregexmid  4745  xpeq1  4765  xpeq2  4766  opthprc  4803  xp11m  5203  funopg  5388  dffo4  5827  funopdmsn  5866  elunirn  5941  f1oiso  6001  canth  6003  eusvobj2  6038  acexmidlema  6043  acexmidlemb  6044  acexmidlemab  6046  acexmidlem2  6049  mpoeq123  6114  oprssdmm  6367  unielxp  6370  cnvf1o  6423  smoel  6533  tfr0dm  6555  frecabcl  6632  nnsucelsuc  6726  nntri3or  6728  nntri2  6729  nntri3  6732  nndceq  6734  nnmordi  6751  nnaordex  6763  elqsn0m  6839  qsel  6848  mapsnd  6925  mapsn  6927  en2m  7068  pw2f1odclem  7089  findcard2s  7149  elssdc  7164  eqsndc  7165  undifdcss  7185  fissfi  7218  2omap  7271  ctssdclemr  7405  nnnninf2  7420  exmidonfinlem  7498  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  finacn  7513  exmidaclem  7517  exmidontriimlem3  7532  exmidontriimlem4  7533  exmidontriim  7534  iftrueb01  7535  pw1ne3  7542  sucpw1ne3  7544  sucpw1nel3  7545  onntri35  7549  acnccim  7588  elni2  7631  addnidpig  7653  elinp  7791  suplocexprlemdisj  8037  suplocexprlemub  8040  pitonn  8165  peano1nnnn  8169  peano2nnnn  8170  peano5nnnn  8209  sup3exmid  9233  peano5nni  9242  1nn  9250  peano2nn  9251  dfuzi  9691  uz11  9880  elfzonlteqm1  10559  frec2uzltd  10769  0tonninf  10806  1tonninf  10807  hashfibclem  11210  wrdsymb0  11261  lsw0  11276  swrdwrdsymbg  11360  sumeq1  12044  prodeq1f  12242  nninfctlemfo  12740  ballotfilemcdc  13146  ctiunct  13208  ssomct  13213  issubm  13702  isnsg  13936  releqgg  13954  eqgex  13955  resghm  13994  ghmeql  14001  issubrg  14383  lmodfopnelem2  14490  islssm  14522  islssmg  14523  lspsneq0  14591  istopg  14881  fiinbas  14931  topbas  14949  epttop  14972  restbasg  15050  icnpimaex  15093  lmcvg  15099  iscnp4  15100  cncnpi  15110  cnconst2  15115  cnptoprest  15121  cnptoprest2  15122  cnpdis  15124  lmss  15128  lmff  15131  txbas  15140  eltx  15141  txcnp  15153  txlm  15161  blssps  15309  blss  15310  blssexps  15311  blssex  15312  neibl  15373  metss  15376  metrest  15388  xmettx  15392  metcnp3  15393  tgioo  15436  tgqioo  15437  uhgrm  16090  lpvtx  16091  incistruhgr  16102  umgrnloopv  16126  uhgredgm  16148  uhgrvtxedgiedgb  16155  upgredg2vtx  16160  uhgr2edg  16218  umgrvad2edg  16223  usgredg4  16227  uspgredg2vlem  16232  ushgredgedg  16238  subgruhgredgdm  16282  vtxd0nedgbfi  16311  1loopgrvd2fi  16317  wlk1walkdom  16371  bdsep2  16673  bdzfauscl  16677  bj-indeq  16716  bj-nn0suc0  16737  bj-nnelirr  16740  bj-peano4  16742  bj-inf2vnlem2  16758  bj-nn0sucALT  16765  bj-findis  16766  strcollnft  16771  sscoll2  16775  nninfsellemdc  16805  nninfsellemqall  16810  nnnninfex  16817