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  5795  funopdmsn  5834  elunirn  5907  f1oiso  5967  canth  5969  eusvobj2  6004  acexmidlema  6009  acexmidlemb  6010  acexmidlemab  6012  acexmidlem2  6015  mpoeq123  6080  oprssdmm  6334  unielxp  6337  cnvf1o  6390  smoel  6466  tfr0dm  6488  frecabcl  6565  nnsucelsuc  6659  nntri3or  6661  nntri2  6662  nntri3  6665  nndceq  6667  nnmordi  6684  nnaordex  6696  elqsn0m  6772  qsel  6781  mapsn  6859  en2m  6999  pw2f1odclem  7020  findcard2s  7079  elssdc  7094  eqsndc  7095  undifdcss  7115  ctssdclemr  7311  nnnninf2  7326  exmidonfinlem  7404  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  finacn  7419  exmidaclem  7423  exmidontriimlem3  7438  exmidontriimlem4  7439  exmidontriim  7440  iftrueb01  7441  pw1ne3  7448  sucpw1ne3  7450  sucpw1nel3  7451  onntri35  7455  acnccim  7491  elni2  7534  addnidpig  7556  elinp  7694  suplocexprlemdisj  7940  suplocexprlemub  7943  pitonn  8068  peano1nnnn  8072  peano2nnnn  8073  peano5nnnn  8112  sup3exmid  9137  peano5nni  9146  1nn  9154  peano2nn  9155  dfuzi  9590  uz11  9779  elfzonlteqm1  10455  frec2uzltd  10665  0tonninf  10702  1tonninf  10703  wrdsymb0  11146  lsw0  11161  swrdwrdsymbg  11245  sumeq1  11916  prodeq1f  12114  nninfctlemfo  12612  ctiunct  13062  ssomct  13067  issubm  13556  isnsg  13790  releqgg  13808  eqgex  13809  resghm  13848  ghmeql  13855  issubrg  14237  lmodfopnelem2  14341  islssm  14373  islssmg  14374  lspsneq0  14442  istopg  14725  fiinbas  14775  topbas  14793  epttop  14816  restbasg  14894  icnpimaex  14937  lmcvg  14943  iscnp4  14944  cncnpi  14954  cnconst2  14959  cnptoprest  14965  cnptoprest2  14966  cnpdis  14968  lmss  14972  lmff  14975  txbas  14984  eltx  14985  txcnp  14997  txlm  15005  blssps  15153  blss  15154  blssexps  15155  blssex  15156  neibl  15217  metss  15220  metrest  15232  xmettx  15236  metcnp3  15237  tgioo  15280  tgqioo  15281  uhgrm  15931  lpvtx  15932  incistruhgr  15943  umgrnloopv  15967  uhgredgm  15989  uhgrvtxedgiedgb  15996  upgredg2vtx  16001  uhgr2edg  16059  umgrvad2edg  16064  usgredg4  16068  uspgredg2vlem  16073  ushgredgedg  16079  subgruhgredgdm  16123  vtxd0nedgbfi  16152  1loopgrvd2fi  16158  wlk1walkdom  16212  bdsep2  16484  bdzfauscl  16488  bj-indeq  16527  bj-nn0suc0  16548  bj-nnelirr  16551  bj-peano4  16553  bj-inf2vnlem2  16569  bj-nn0sucALT  16576  bj-findis  16577  strcollnft  16582  sscoll2  16586  2omap  16597  nninfsellemdc  16615  nninfsellemqall  16620  nnnninfex  16627