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  5785  funopdmsn  5823  elunirn  5896  f1oiso  5956  canth  5958  eusvobj2  5993  acexmidlema  5998  acexmidlemb  5999  acexmidlemab  6001  acexmidlem2  6004  mpoeq123  6069  oprssdmm  6323  unielxp  6326  cnvf1o  6377  smoel  6452  tfr0dm  6474  frecabcl  6551  nnsucelsuc  6645  nntri3or  6647  nntri2  6648  nntri3  6651  nndceq  6653  nnmordi  6670  nnaordex  6682  elqsn0m  6758  qsel  6767  mapsn  6845  en2m  6982  pw2f1odclem  7003  findcard2s  7060  elssdc  7075  eqsndc  7076  undifdcss  7096  ctssdclemr  7290  nnnninf2  7305  exmidonfinlem  7382  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  finacn  7397  exmidaclem  7401  exmidontriimlem3  7416  exmidontriimlem4  7417  exmidontriim  7418  iftrueb01  7419  pw1ne3  7426  sucpw1ne3  7428  sucpw1nel3  7429  onntri35  7433  acnccim  7469  elni2  7512  addnidpig  7534  elinp  7672  suplocexprlemdisj  7918  suplocexprlemub  7921  pitonn  8046  peano1nnnn  8050  peano2nnnn  8051  peano5nnnn  8090  sup3exmid  9115  peano5nni  9124  1nn  9132  peano2nn  9133  dfuzi  9568  uz11  9757  elfzonlteqm1  10428  frec2uzltd  10637  0tonninf  10674  1tonninf  10675  wrdsymb0  11117  lsw0  11132  swrdwrdsymbg  11212  sumeq1  11882  prodeq1f  12079  nninfctlemfo  12577  ctiunct  13027  ssomct  13032  issubm  13521  isnsg  13755  releqgg  13773  eqgex  13774  resghm  13813  ghmeql  13820  issubrg  14201  lmodfopnelem2  14305  islssm  14337  islssmg  14338  lspsneq0  14406  istopg  14689  fiinbas  14739  topbas  14757  epttop  14780  restbasg  14858  icnpimaex  14901  lmcvg  14907  iscnp4  14908  cncnpi  14918  cnconst2  14923  cnptoprest  14929  cnptoprest2  14930  cnpdis  14932  lmss  14936  lmff  14939  txbas  14948  eltx  14949  txcnp  14961  txlm  14969  blssps  15117  blss  15118  blssexps  15119  blssex  15120  neibl  15181  metss  15184  metrest  15196  xmettx  15200  metcnp3  15201  tgioo  15244  tgqioo  15245  uhgrm  15894  lpvtx  15895  incistruhgr  15906  umgrnloopv  15930  uhgredgm  15950  uhgrvtxedgiedgb  15957  upgredg2vtx  15962  uhgr2edg  16020  umgrvad2edg  16025  usgredg4  16029  uspgredg2vlem  16034  ushgredgedg  16040  vtxd0nedgbfi  16059  wlk1walkdom  16105  bdsep2  16332  bdzfauscl  16336  bj-indeq  16375  bj-nn0suc0  16396  bj-nnelirr  16399  bj-peano4  16401  bj-inf2vnlem2  16417  bj-nn0sucALT  16424  bj-findis  16425  strcollnft  16430  sscoll2  16434  2omap  16446  nninfsellemdc  16464  nninfsellemqall  16469  nnnninfex  16476