Theorem eleq2 2142

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 2075	. . . . . 6 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
2	1	biimpi 118	. . . . 5 |- ( A = B -> A. x ( x e. A <-> x e. B ) )
3	2	19.21bi 1490	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
4	3	anbi2d 451	. . 3 |- ( A = B -> ( ( x = C /\ x e. A ) <-> ( x = C /\ x e. B ) ) )
5	4	exbidv 1746	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2077	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2077	. 2 |- ( C e. B <-> E. x ( x = C /\ x e. B ) )
8	5, 6, 7	3bitr4g 221	1 |- ( A = B -> ( C e. A <-> C e. B ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   A.wal 1282   = wceq 1284   E.wex 1421   e. wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  eleq12  2143  eleq2i  2145  eleq2d  2148  nelneq2  2180  clelsb4  2184  dvelimdc  2238  nelne1  2335  neleq2  2344  raleqf  2545  rexeqf  2546  reueq1f  2547  rmoeq1f  2548  rabeqf  2594  clel3g  2729  clel4  2731  sbcbi2  2864  sbcel2gv  2877  sbnfc2  2962  difeq2  3084  uneq1  3119  ineq1  3160  n0i  3256  disjel  3298  exsnrex  3435  sneqr  3552  preqr1g  3558  preqr1  3560  preq12b  3562  prel12  3563  elunii  3606  eluniab  3613  ssuni  3623  elinti  3645  elintab  3647  intss1  3651  intmin  3656  intab  3665  iineq2  3695  dfiin2g  3711  breq  3787  axsep2  3897  zfauscl  3898  inuni  3930  rext  3970  intid  3979  mss  3981  opth1  3991  opeqex  4004  frforeq3  4102  frirrg  4105  limeq  4132  nsuceq0g  4173  suctr  4176  snnex  4199  uniuni  4201  iunpw  4229  ordtriexmidlem  4263  ordtriexmidlem2  4264  ordtriexmid  4265  ordtri2orexmid  4266  ontr2exmid  4268  ordtri2or2exmidlem  4269  onsucelsucexmidlem  4272  onsucelsucexmid  4273  ordsucunielexmid  4274  regexmidlem1  4276  reg2exmidlema  4277  regexmid  4278  reg2exmid  4279  elirr  4284  en2lp  4297  suc11g  4300  dtruex  4302  ordsoexmid  4305  nlimsucg  4309  onintexmid  4315  reg3exmidlemwe  4321  reg3exmid  4322  peano5  4339  limom  4354  0elnn  4358  nn0eln0  4359  nnregexmid  4360  xpeq1  4377  xpeq2  4378  opthprc  4409  xp11m  4779  funopg  4954  dffo4  5336  elunirn  5426  f1oiso  5485  eusvobj2  5518  acexmidlema  5523  acexmidlemb  5524  acexmidlemab  5526  acexmidlem2  5529  mpt2eq123  5584  unielxp  5820  cnvf1o  5866  smoel  5938  tfr0  5960  nnsucelsuc  6093  nntri3or  6095  nntri2  6096  nntri3  6098  nndceq  6100  nnmordi  6112  nnaordex  6123  elqsn0m  6197  qsel  6206  findcard2s  6374  elni2  6504  addnidpig  6526  elinp  6664  pitonn  7016  peano1nnnn  7020  peano2nnnn  7021  peano5nnnn  7058  peano5nni  8042  1nn  8050  peano2nn  8051  dfuzi  8457  uz11  8641  elfzonlteqm1  9219  frec2uzltd  9405  bdsep2  10677  bdzfauscl  10681  bj-indeq  10724  bj-nn0suc0  10745  bj-nnelirr  10748  bj-peano4  10750  bj-inf2vnlem2  10766  bj-nn0sucALT  10773  bj-findis  10774