Theorem eleq2 2293

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 2223	. . . . . 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 1604	. . . 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 1871	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2225	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2225	. 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 1393   = wceq 1395   E.wex 1538   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12  2294  eleq2i  2296  eleq2d  2299  nelneq2  2331  clelsb2  2335  dvelimdc  2393  nelne1  2490  neleq2  2500  raleqf  2724  rexeqf  2725  reueq1f  2726  rmoeq1f  2727  rabeqf  2789  clel3g  2937  clel4  2939  sbcbi2  3079  sbcel2gv  3092  csbeq2  3148  sbnfc2  3185  difeq2  3316  uneq1  3351  ineq1  3398  nel02  3496  n0i  3497  disjel  3546  exsnrex  3708  sneqr  3838  preqr1g  3844  preqr1  3846  preq12b  3848  prel12  3849  elunii  3893  eluniab  3900  ssuni  3910  elinti  3932  elintab  3934  intss1  3938  intmin  3943  intab  3952  iineq2  3982  dfiin2g  3998  breq  4085  axsep2  4203  zfauscl  4204  inuni  4239  exmidexmid  4280  ss1o0el1  4281  exmid01  4282  exmidundif  4290  exmidundifim  4291  rext  4301  intid  4310  mss  4312  opth1  4322  opeqex  4336  frforeq3  4438  frirrg  4441  limeq  4468  nsuceq0g  4509  suctr  4512  snnex  4539  uniuni  4542  iunpw  4571  ordtriexmidlem  4611  ordtriexmidlem2  4612  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  ontr2exmid  4617  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  onsucelsucexmid  4622  ordsucunielexmid  4623  regexmidlem1  4625  reg2exmidlema  4626  regexmid  4627  reg2exmid  4628  elirr  4633  en2lp  4646  suc11g  4649  dtruex  4651  ordsoexmid  4654  nlimsucg  4658  onintexmid  4665  reg3exmidlemwe  4671  reg3exmid  4672  peano5  4690  limom  4706  0elnn  4711  nn0eln0  4712  nnregexmid  4713  xpeq1  4733  xpeq2  4734  opthprc  4770  xp11m  5167  funopg  5352  dffo4  5783  funopdmsn  5819  elunirn  5890  f1oiso  5950  canth  5952  eusvobj2  5987  acexmidlema  5992  acexmidlemb  5993  acexmidlemab  5995  acexmidlem2  5998  mpoeq123  6063  oprssdmm  6317  unielxp  6320  cnvf1o  6371  smoel  6446  tfr0dm  6468  frecabcl  6545  nnsucelsuc  6637  nntri3or  6639  nntri2  6640  nntri3  6643  nndceq  6645  nnmordi  6662  nnaordex  6674  elqsn0m  6750  qsel  6759  mapsn  6837  en2m  6974  pw2f1odclem  6995  findcard2s  7052  undifdcss  7085  ctssdclemr  7279  nnnninf2  7294  exmidonfinlem  7371  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  finacn  7386  exmidaclem  7390  exmidontriimlem3  7405  exmidontriimlem4  7406  exmidontriim  7407  iftrueb01  7408  pw1ne3  7415  sucpw1ne3  7417  sucpw1nel3  7418  onntri35  7422  acnccim  7458  elni2  7501  addnidpig  7523  elinp  7661  suplocexprlemdisj  7907  suplocexprlemub  7910  pitonn  8035  peano1nnnn  8039  peano2nnnn  8040  peano5nnnn  8079  sup3exmid  9104  peano5nni  9113  1nn  9121  peano2nn  9122  dfuzi  9557  uz11  9745  elfzonlteqm1  10416  frec2uzltd  10625  0tonninf  10662  1tonninf  10663  wrdsymb0  11104  lsw0  11119  swrdwrdsymbg  11196  sumeq1  11866  prodeq1f  12063  nninfctlemfo  12561  ctiunct  13011  ssomct  13016  issubm  13505  isnsg  13739  releqgg  13757  eqgex  13758  resghm  13797  ghmeql  13804  issubrg  14185  lmodfopnelem2  14289  islssm  14321  islssmg  14322  lspsneq0  14390  istopg  14673  fiinbas  14723  topbas  14741  epttop  14764  restbasg  14842  icnpimaex  14885  lmcvg  14891  iscnp4  14892  cncnpi  14902  cnconst2  14907  cnptoprest  14913  cnptoprest2  14914  cnpdis  14916  lmss  14920  lmff  14923  txbas  14932  eltx  14933  txcnp  14945  txlm  14953  blssps  15101  blss  15102  blssexps  15103  blssex  15104  neibl  15165  metss  15168  metrest  15180  xmettx  15184  metcnp3  15185  tgioo  15228  tgqioo  15229  uhgrm  15878  lpvtx  15879  incistruhgr  15890  umgrnloopv  15914  uhgredgm  15934  uhgrvtxedgiedgb  15941  upgredg2vtx  15946  uhgr2edg  16004  umgrvad2edg  16009  usgredg4  16013  uspgredg2vlem  16018  ushgredgedg  16024  wlk1walkdom  16070  bdsep2  16249  bdzfauscl  16253  bj-indeq  16292  bj-nn0suc0  16313  bj-nnelirr  16316  bj-peano4  16318  bj-inf2vnlem2  16334  bj-nn0sucALT  16341  bj-findis  16342  strcollnft  16347  sscoll2  16351  2omap  16359  nninfsellemdc  16376  nninfsellemqall  16381  nnnninfex  16388