Theorem eleq2 2295

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 2225	. . . . . 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 1606	. . . 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 1873	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2227	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2227	. 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 1395   = wceq 1397   E.wex 1540   e. wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12  2296  eleq2i  2298  eleq2d  2301  nelneq2  2333  clelsb2  2337  dvelimdc  2395  nelne1  2492  neleq2  2502  raleqf  2726  rexeqf  2727  reueq1f  2728  rmoeq1f  2729  rabeqf  2792  clel3g  2940  clel4  2942  sbcbi2  3082  sbcel2gv  3095  csbeq2  3151  sbnfc2  3188  difeq2  3319  uneq1  3354  ineq1  3401  nel02  3499  n0i  3500  disjel  3549  exsnrex  3711  sneqr  3843  preqr1g  3849  preqr1  3851  preq12b  3853  prel12  3854  elunii  3898  eluniab  3905  ssuni  3915  elinti  3937  elintab  3939  intss1  3943  intmin  3948  intab  3957  iineq2  3987  dfiin2g  4003  breq  4090  axsep2  4208  zfauscl  4209  inuni  4245  exmidexmid  4286  ss1o0el1  4287  exmid01  4288  exmidundif  4296  exmidundifim  4297  rext  4307  intid  4316  mss  4318  opth1  4328  opeqex  4342  frforeq3  4444  frirrg  4447  limeq  4474  nsuceq0g  4515  suctr  4518  snnex  4545  uniuni  4548  iunpw  4577  ordtriexmidlem  4617  ordtriexmidlem2  4618  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  ontr2exmid  4623  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  onsucelsucexmid  4628  ordsucunielexmid  4629  regexmidlem1  4631  reg2exmidlema  4632  regexmid  4633  reg2exmid  4634  elirr  4639  en2lp  4652  suc11g  4655  dtruex  4657  ordsoexmid  4660  nlimsucg  4664  onintexmid  4671  reg3exmidlemwe  4677  reg3exmid  4678  peano5  4696  limom  4712  0elnn  4717  nn0eln0  4718  nnregexmid  4719  xpeq1  4739  xpeq2  4740  opthprc  4777  xp11m  5175  funopg  5360  dffo4  5796  funopdmsn  5835  elunirn  5910  f1oiso  5970  canth  5972  eusvobj2  6007  acexmidlema  6012  acexmidlemb  6013  acexmidlemab  6015  acexmidlem2  6018  mpoeq123  6083  oprssdmm  6337  unielxp  6340  cnvf1o  6393  smoel  6469  tfr0dm  6491  frecabcl  6568  nnsucelsuc  6662  nntri3or  6664  nntri2  6665  nntri3  6668  nndceq  6670  nnmordi  6687  nnaordex  6699  elqsn0m  6775  qsel  6784  mapsn  6862  en2m  7002  pw2f1odclem  7023  findcard2s  7082  elssdc  7097  eqsndc  7098  undifdcss  7118  ctssdclemr  7314  nnnninf2  7329  exmidonfinlem  7407  exmidfodomrlemr  7416  exmidfodomrlemrALT  7417  finacn  7422  exmidaclem  7426  exmidontriimlem3  7441  exmidontriimlem4  7442  exmidontriim  7443  iftrueb01  7444  pw1ne3  7451  sucpw1ne3  7453  sucpw1nel3  7454  onntri35  7458  acnccim  7494  elni2  7537  addnidpig  7559  elinp  7697  suplocexprlemdisj  7943  suplocexprlemub  7946  pitonn  8071  peano1nnnn  8075  peano2nnnn  8076  peano5nnnn  8115  sup3exmid  9140  peano5nni  9149  1nn  9157  peano2nn  9158  dfuzi  9593  uz11  9782  elfzonlteqm1  10459  frec2uzltd  10669  0tonninf  10706  1tonninf  10707  wrdsymb0  11153  lsw0  11168  swrdwrdsymbg  11252  sumeq1  11936  prodeq1f  12134  nninfctlemfo  12632  ctiunct  13082  ssomct  13087  issubm  13576  isnsg  13810  releqgg  13828  eqgex  13829  resghm  13868  ghmeql  13875  issubrg  14257  lmodfopnelem2  14361  islssm  14393  islssmg  14394  lspsneq0  14462  istopg  14750  fiinbas  14800  topbas  14818  epttop  14841  restbasg  14919  icnpimaex  14962  lmcvg  14968  iscnp4  14969  cncnpi  14979  cnconst2  14984  cnptoprest  14990  cnptoprest2  14991  cnpdis  14993  lmss  14997  lmff  15000  txbas  15009  eltx  15010  txcnp  15022  txlm  15030  blssps  15178  blss  15179  blssexps  15180  blssex  15181  neibl  15242  metss  15245  metrest  15257  xmettx  15261  metcnp3  15262  tgioo  15305  tgqioo  15306  uhgrm  15956  lpvtx  15957  incistruhgr  15968  umgrnloopv  15992  uhgredgm  16014  uhgrvtxedgiedgb  16021  upgredg2vtx  16026  uhgr2edg  16084  umgrvad2edg  16089  usgredg4  16093  uspgredg2vlem  16098  ushgredgedg  16104  subgruhgredgdm  16148  vtxd0nedgbfi  16177  1loopgrvd2fi  16183  wlk1walkdom  16237  bdsep2  16540  bdzfauscl  16544  bj-indeq  16583  bj-nn0suc0  16604  bj-nnelirr  16607  bj-peano4  16609  bj-inf2vnlem2  16625  bj-nn0sucALT  16632  bj-findis  16633  strcollnft  16638  sscoll2  16642  2omap  16653  nninfsellemdc  16671  nninfsellemqall  16676  nnnninfex  16683