Theorem eleq2 2296

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 2226	. . . . . 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 1607	. . . 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 1874	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2228	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2228	. 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 1396   = wceq 1398   E.wex 1541   e. wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

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

This theorem is referenced by:  eleq12  2297  eleq2i  2299  eleq2d  2302  nelneq2  2334  clelsb2  2338  dvelimdc  2405  nelne1  2502  neleq2  2512  raleqf  2736  rexeqf  2737  reueq1f  2738  rmoeq1f  2739  rabeqf  2802  clel3g  2950  clel4  2952  sbcbi2  3092  sbcel2gv  3105  csbeq2  3161  sbnfc2  3198  difeq2  3330  uneq1  3365  ineq1  3412  nel02  3510  n0i  3511  disjel  3560  exsnrex  3724  sneqr  3857  preqr1g  3863  preqr1  3865  preq12b  3867  prel12  3868  elunii  3912  eluniab  3919  ssuni  3929  elinti  3951  elintab  3953  intss1  3957  intmin  3962  intab  3971  iineq2  4001  dfiin2g  4017  breq  4104  axsep2  4222  zfauscl  4223  inuni  4259  exmidexmid  4301  ss1o0el1  4302  exmid01  4303  exmidundif  4311  exmidundifim  4312  rext  4322  intid  4331  mss  4333  opth1  4343  opeqex  4357  frforeq3  4459  frirrg  4462  limeq  4489  nsuceq0g  4530  suctr  4533  snnex  4560  uniuni  4563  iunpw  4592  ordtriexmidlem  4632  ordtriexmidlem2  4633  ordtriexmid  4634  ontriexmidim  4635  ordtri2orexmid  4636  ontr2exmid  4638  ordtri2or2exmidlem  4639  onsucelsucexmidlem  4642  onsucelsucexmid  4643  ordsucunielexmid  4644  regexmidlem1  4646  reg2exmidlema  4647  regexmid  4648  reg2exmid  4649  elirr  4654  en2lp  4667  suc11g  4670  dtruex  4672  ordsoexmid  4675  nlimsucg  4679  onintexmid  4686  reg3exmidlemwe  4692  reg3exmid  4693  peano5  4711  limom  4727  0elnn  4732  nn0eln0  4733  nnregexmid  4734  xpeq1  4754  xpeq2  4755  opthprc  4792  xp11m  5192  funopg  5377  dffo4  5816  funopdmsn  5855  elunirn  5930  f1oiso  5990  canth  5992  eusvobj2  6027  acexmidlema  6032  acexmidlemb  6033  acexmidlemab  6035  acexmidlem2  6038  mpoeq123  6103  oprssdmm  6356  unielxp  6359  cnvf1o  6412  smoel  6522  tfr0dm  6544  frecabcl  6621  nnsucelsuc  6715  nntri3or  6717  nntri2  6718  nntri3  6721  nndceq  6723  nnmordi  6740  nnaordex  6752  elqsn0m  6828  qsel  6837  mapsnd  6914  mapsn  6916  en2m  7057  pw2f1odclem  7078  findcard2s  7138  elssdc  7153  eqsndc  7154  undifdcss  7174  fissfi  7207  2omap  7260  ctssdclemr  7394  nnnninf2  7409  exmidonfinlem  7487  exmidfodomrlemr  7496  exmidfodomrlemrALT  7497  finacn  7502  exmidaclem  7506  exmidontriimlem3  7521  exmidontriimlem4  7522  exmidontriim  7523  iftrueb01  7524  pw1ne3  7531  sucpw1ne3  7533  sucpw1nel3  7534  onntri35  7538  acnccim  7574  elni2  7617  addnidpig  7639  elinp  7777  suplocexprlemdisj  8023  suplocexprlemub  8026  pitonn  8151  peano1nnnn  8155  peano2nnnn  8156  peano5nnnn  8195  sup3exmid  9219  peano5nni  9228  1nn  9236  peano2nn  9237  dfuzi  9674  uz11  9863  elfzonlteqm1  10541  frec2uzltd  10751  0tonninf  10788  1tonninf  10789  wrdsymb0  11235  lsw0  11250  swrdwrdsymbg  11334  sumeq1  12018  prodeq1f  12216  nninfctlemfo  12714  ctiunct  13165  ssomct  13170  issubm  13659  isnsg  13893  releqgg  13911  eqgex  13912  resghm  13951  ghmeql  13958  issubrg  14340  lmodfopnelem2  14445  islssm  14477  islssmg  14478  lspsneq0  14546  istopg  14834  fiinbas  14884  topbas  14902  epttop  14925  restbasg  15003  icnpimaex  15046  lmcvg  15052  iscnp4  15053  cncnpi  15063  cnconst2  15068  cnptoprest  15074  cnptoprest2  15075  cnpdis  15077  lmss  15081  lmff  15084  txbas  15093  eltx  15094  txcnp  15106  txlm  15114  blssps  15262  blss  15263  blssexps  15264  blssex  15265  neibl  15326  metss  15329  metrest  15341  xmettx  15345  metcnp3  15346  tgioo  15389  tgqioo  15390  uhgrm  16043  lpvtx  16044  incistruhgr  16055  umgrnloopv  16079  uhgredgm  16101  uhgrvtxedgiedgb  16108  upgredg2vtx  16113  uhgr2edg  16171  umgrvad2edg  16176  usgredg4  16180  uspgredg2vlem  16185  ushgredgedg  16191  subgruhgredgdm  16235  vtxd0nedgbfi  16264  1loopgrvd2fi  16270  wlk1walkdom  16324  bdsep2  16626  bdzfauscl  16630  bj-indeq  16669  bj-nn0suc0  16690  bj-nnelirr  16693  bj-peano4  16695  bj-inf2vnlem2  16711  bj-nn0sucALT  16718  bj-findis  16719  strcollnft  16724  sscoll2  16728  nninfsellemdc  16758  nninfsellemqall  16763  nnnninfex  16770