Theorem eleq2 2101

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 2034	. . . . . 6 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
2	1	biimpi 113	. . . . 5 |- ( A = B -> A. x ( x e. A <-> x e. B ) )
3	2	19.21bi 1450	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
4	3	anbi2d 437	. . 3 |- ( A = B -> ( ( x = C /\ x e. A ) <-> ( x = C /\ x e. B ) ) )
5	4	exbidv 1706	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2036	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2036	. 2 |- ( C e. B <-> E. x ( x = C /\ x e. B ) )
8	5, 6, 7	3bitr4g 212	1 |- ( A = B -> ( C e. A <-> C e. B ) )

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   A.wal 1241   = wceq 1243   E.wex 1381   e. wcel 1393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036

This theorem is referenced by:  eleq12  2102  eleq2i  2104  eleq2d  2107  nelneq2  2139  clelsb4  2143  dvelimdc  2197  nelne1  2295  neleq2  2302  raleqf  2501  rexeqf  2502  reueq1f  2503  rmoeq1f  2504  rabeqf  2550  clel3g  2678  clel4  2680  sbcel2gv  2822  sbnfc2  2906  difeq2  3056  uneq1  3090  ineq1  3131  n0i  3229  disjel  3274  exsnrex  3413  sneqr  3531  preqr1g  3537  preqr1  3539  preq12b  3541  prel12  3542  elunii  3585  eluniab  3592  ssuni  3602  elinti  3624  elintab  3626  intss1  3630  intmin  3635  intab  3644  iineq2  3674  dfiin2g  3690  breq  3766  axsep2  3876  zfauscl  3877  inuni  3909  rext  3951  intid  3960  mss  3962  opth1  3973  opeqex  3986  frforeq3  4084  frirrg  4087  limeq  4114  nsuceq0g  4155  suctr  4158  snnex  4181  uniuni  4183  iunpw  4211  ordtriexmidlem  4245  ordtriexmidlem2  4246  ordtriexmid  4247  ordtri2orexmid  4248  ontr2exmid  4250  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  onsucelsucexmid  4255  ordsucunielexmid  4256  regexmidlem1  4258  reg2exmidlema  4259  regexmid  4260  reg2exmid  4261  elirr  4266  en2lp  4278  suc11g  4281  dtruex  4283  ordsoexmid  4286  nlimsucg  4290  onpsssuc  4295  onintexmid  4297  reg3exmidlemwe  4303  reg3exmid  4304  peano5  4321  limom  4336  0elnn  4340  nn0eln0  4341  nnregexmid  4342  xpeq1  4359  xpeq2  4360  opthprc  4391  xp11m  4759  funopg  4934  dffo4  5315  elunirn  5405  f1oiso  5465  eusvobj2  5498  acexmidlema  5503  acexmidlemb  5504  acexmidlemab  5506  acexmidlem2  5509  mpt2eq123  5564  unielxp  5800  cnvf1o  5846  smoel  5915  tfr0  5937  nnsucelsuc  6070  nntri3or  6072  nntri2  6073  nntri3  6075  nndceq  6077  nnmordi  6089  nnaordex  6100  elqsn0m  6174  qsel  6183  findcard2s  6347  elni2  6412  addnidpig  6434  elinp  6572  pitonn  6924  peano1nnnn  6928  peano2nnnn  6929  peano5nnnn  6966  peano5nni  7917  1nn  7925  peano2nn  7926  dfuzi  8348  uz11  8495  elfzonlteqm1  9066  frec2uzltd  9189  bdsep2  10006  bdzfauscl  10010  bj-indeq  10053  bj-nn0suc0  10075  bj-nnelirr  10078  bj-peano4  10080  bj-inf2vnlem2  10096  bj-nn0sucALT  10103  bj-findis  10104