Theorem eleq2 2151

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 2082	. . . . . 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 1495	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
4	3	anbi2d 452	. . 3 |- ( A = B -> ( ( x = C /\ x e. A ) <-> ( x = C /\ x e. B ) ) )
5	4	exbidv 1753	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2084	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2084	. 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 1287   = wceq 1289   E.wex 1426   e. wcel 1438

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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084

This theorem is referenced by:  eleq12  2152  eleq2i  2154  eleq2d  2157  nelneq2  2189  clelsb4  2193  dvelimdc  2248  nelne1  2345  neleq2  2355  raleqf  2558  rexeqf  2559  reueq1f  2560  rmoeq1f  2561  rabeqf  2609  clel3g  2749  clel4  2751  sbcbi2  2887  sbcel2gv  2900  sbnfc2  2986  difeq2  3110  uneq1  3145  ineq1  3192  n0i  3289  disjel  3334  exsnrex  3480  sneqr  3599  preqr1g  3605  preqr1  3607  preq12b  3609  prel12  3610  elunii  3653  eluniab  3660  ssuni  3670  elinti  3692  elintab  3694  intss1  3698  intmin  3703  intab  3712  iineq2  3742  dfiin2g  3758  breq  3839  axsep2  3950  zfauscl  3951  inuni  3983  exmidexmid  4022  exmid01  4023  exmidundif  4026  rext  4033  intid  4042  mss  4044  opth1  4054  opeqex  4067  frforeq3  4165  frirrg  4168  limeq  4195  nsuceq0g  4236  suctr  4239  snnex  4262  uniuni  4264  iunpw  4292  ordtriexmidlem  4326  ordtriexmidlem2  4327  ordtriexmid  4328  ordtri2orexmid  4329  ontr2exmid  4331  ordtri2or2exmidlem  4332  onsucelsucexmidlem  4335  onsucelsucexmid  4336  ordsucunielexmid  4337  regexmidlem1  4339  reg2exmidlema  4340  regexmid  4341  reg2exmid  4342  elirr  4347  en2lp  4360  suc11g  4363  dtruex  4365  ordsoexmid  4368  nlimsucg  4372  onintexmid  4378  reg3exmidlemwe  4384  reg3exmid  4385  peano5  4403  limom  4418  0elnn  4422  nn0eln0  4423  nnregexmid  4424  xpeq1  4442  xpeq2  4443  opthprc  4477  xp11m  4856  funopg  5034  dffo4  5431  elunirn  5527  f1oiso  5587  eusvobj2  5620  acexmidlema  5625  acexmidlemb  5626  acexmidlemab  5628  acexmidlem2  5631  mpt2eq123  5690  unielxp  5926  cnvf1o  5972  smoel  6047  tfr0dm  6069  frecabcl  6146  nnsucelsuc  6234  nntri3or  6236  nntri2  6237  nntri3  6240  nndceq  6242  nnmordi  6255  nnaordex  6266  elqsn0m  6340  qsel  6349  mapsn  6427  findcard2s  6586  undifdcss  6613  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  elni2  6852  addnidpig  6874  elinp  7012  pitonn  7364  peano1nnnn  7368  peano2nnnn  7369  peano5nnnn  7406  peano5nni  8397  1nn  8405  peano2nn  8406  dfuzi  8826  uz11  9010  elfzonlteqm1  9586  frec2uzltd  9775  0tonninf  9810  1tonninf  9811  sumeq1  10708  bdsep2  11434  bdzfauscl  11438  bj-indeq  11481  bj-nn0suc0  11502  bj-nnelirr  11505  bj-peano4  11507  bj-inf2vnlem2  11523  bj-nn0sucALT  11530  bj-findis  11531  nninfsellemdc  11559  nninfsellemqall  11564