Theorem eleq2 2203

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 2133	. . . . . 6 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
2	1	biimpi 119	. . . . 5 |- ( A = B -> A. x ( x e. A <-> x e. B ) )
3	2	19.21bi 1537	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
4	3	anbi2d 459	. . 3 |- ( A = B -> ( ( x = C /\ x e. A ) <-> ( x = C /\ x e. B ) ) )
5	4	exbidv 1797	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2135	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2135	. 2 |- ( C e. B <-> E. x ( x = C /\ x e. B ) )
8	5, 6, 7	3bitr4g 222	1 |- ( A = B -> ( C e. A <-> C e. B ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1329   = wceq 1331   E.wex 1468   e. wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  eleq12  2204  eleq2i  2206  eleq2d  2209  nelneq2  2241  clelsb4  2245  dvelimdc  2301  nelne1  2398  neleq2  2408  raleqf  2622  rexeqf  2623  reueq1f  2624  rmoeq1f  2625  rabeqf  2676  clel3g  2819  clel4  2821  sbcbi2  2959  sbcel2gv  2972  csbeq2  3026  sbnfc2  3060  difeq2  3188  uneq1  3223  ineq1  3270  n0i  3368  disjel  3417  exsnrex  3566  sneqr  3687  preqr1g  3693  preqr1  3695  preq12b  3697  prel12  3698  elunii  3741  eluniab  3748  ssuni  3758  elinti  3780  elintab  3782  intss1  3786  intmin  3791  intab  3800  iineq2  3830  dfiin2g  3846  breq  3931  axsep2  4047  zfauscl  4048  inuni  4080  exmidexmid  4120  exmid01  4121  exmidundif  4129  exmidundifim  4130  rext  4137  intid  4146  mss  4148  opth1  4158  opeqex  4171  frforeq3  4269  frirrg  4272  limeq  4299  nsuceq0g  4340  suctr  4343  snnex  4369  uniuni  4372  iunpw  4401  ordtriexmidlem  4435  ordtriexmidlem2  4436  ordtriexmid  4437  ordtri2orexmid  4438  ontr2exmid  4440  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  onsucelsucexmid  4445  ordsucunielexmid  4446  regexmidlem1  4448  reg2exmidlema  4449  regexmid  4450  reg2exmid  4451  elirr  4456  en2lp  4469  suc11g  4472  dtruex  4474  ordsoexmid  4477  nlimsucg  4481  onintexmid  4487  reg3exmidlemwe  4493  reg3exmid  4494  peano5  4512  limom  4527  0elnn  4532  nn0eln0  4533  nnregexmid  4534  xpeq1  4553  xpeq2  4554  opthprc  4590  xp11m  4977  funopg  5157  dffo4  5568  elunirn  5667  f1oiso  5727  eusvobj2  5760  acexmidlema  5765  acexmidlemb  5766  acexmidlemab  5768  acexmidlem2  5771  mpoeq123  5830  oprssdmm  6069  unielxp  6072  cnvf1o  6122  smoel  6197  tfr0dm  6219  frecabcl  6296  nnsucelsuc  6387  nntri3or  6389  nntri2  6390  nntri3  6393  nndceq  6395  nnmordi  6412  nnaordex  6423  elqsn0m  6497  qsel  6506  mapsn  6584  findcard2s  6784  undifdcss  6811  ctssdclemr  6997  exmidonfinlem  7049  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  elni2  7122  addnidpig  7144  elinp  7282  suplocexprlemdisj  7528  suplocexprlemub  7531  pitonn  7656  peano1nnnn  7660  peano2nnnn  7661  peano5nnnn  7700  sup3exmid  8715  peano5nni  8723  1nn  8731  peano2nn  8732  dfuzi  9161  uz11  9348  elfzonlteqm1  9987  frec2uzltd  10176  0tonninf  10212  1tonninf  10213  sumeq1  11124  prodeq1f  11321  ctiunct  11953  istopg  12166  fiinbas  12216  topbas  12236  epttop  12259  restbasg  12337  icnpimaex  12380  lmcvg  12386  iscnp4  12387  cncnpi  12397  cnconst2  12402  cnptoprest  12408  cnptoprest2  12409  cnpdis  12411  lmss  12415  lmff  12418  txbas  12427  eltx  12428  txcnp  12440  txlm  12448  blssps  12596  blss  12597  blssexps  12598  blssex  12599  neibl  12660  metss  12663  metrest  12675  xmettx  12679  metcnp3  12680  tgioo  12715  tgqioo  12716  bdsep2  13084  bdzfauscl  13088  bj-indeq  13127  bj-nn0suc0  13148  bj-nnelirr  13151  bj-peano4  13153  bj-inf2vnlem2  13169  bj-nn0sucALT  13176  bj-findis  13177  nninfsellemdc  13206  nninfsellemqall  13211