Theorem eleq2 2271

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 2201	. . . . . 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 1582	. . . 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 1849	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2203	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2203	. 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 1371   = wceq 1373   E.wex 1516   e. wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  eleq12  2272  eleq2i  2274  eleq2d  2277  nelneq2  2309  clelsb2  2313  dvelimdc  2371  nelne1  2468  neleq2  2478  raleqf  2701  rexeqf  2702  reueq1f  2703  rmoeq1f  2704  rabeqf  2766  clel3g  2914  clel4  2916  sbcbi2  3056  sbcel2gv  3069  csbeq2  3125  sbnfc2  3162  difeq2  3293  uneq1  3328  ineq1  3375  nel02  3473  n0i  3474  disjel  3523  exsnrex  3685  sneqr  3814  preqr1g  3820  preqr1  3822  preq12b  3824  prel12  3825  elunii  3869  eluniab  3876  ssuni  3886  elinti  3908  elintab  3910  intss1  3914  intmin  3919  intab  3928  iineq2  3958  dfiin2g  3974  breq  4061  axsep2  4179  zfauscl  4180  inuni  4215  exmidexmid  4256  ss1o0el1  4257  exmid01  4258  exmidundif  4266  exmidundifim  4267  rext  4277  intid  4286  mss  4288  opth1  4298  opeqex  4312  frforeq3  4412  frirrg  4415  limeq  4442  nsuceq0g  4483  suctr  4486  snnex  4513  uniuni  4516  iunpw  4545  ordtriexmidlem  4585  ordtriexmidlem2  4586  ordtriexmid  4587  ontriexmidim  4588  ordtri2orexmid  4589  ontr2exmid  4591  ordtri2or2exmidlem  4592  onsucelsucexmidlem  4595  onsucelsucexmid  4596  ordsucunielexmid  4597  regexmidlem1  4599  reg2exmidlema  4600  regexmid  4601  reg2exmid  4602  elirr  4607  en2lp  4620  suc11g  4623  dtruex  4625  ordsoexmid  4628  nlimsucg  4632  onintexmid  4639  reg3exmidlemwe  4645  reg3exmid  4646  peano5  4664  limom  4680  0elnn  4685  nn0eln0  4686  nnregexmid  4687  xpeq1  4707  xpeq2  4708  opthprc  4744  xp11m  5140  funopg  5324  dffo4  5751  funopdmsn  5787  elunirn  5858  f1oiso  5918  canth  5920  eusvobj2  5953  acexmidlema  5958  acexmidlemb  5959  acexmidlemab  5961  acexmidlem2  5964  mpoeq123  6027  oprssdmm  6280  unielxp  6283  cnvf1o  6334  smoel  6409  tfr0dm  6431  frecabcl  6508  nnsucelsuc  6600  nntri3or  6602  nntri2  6603  nntri3  6606  nndceq  6608  nnmordi  6625  nnaordex  6637  elqsn0m  6713  qsel  6722  mapsn  6800  en2m  6937  pw2f1odclem  6956  findcard2s  7013  undifdcss  7046  ctssdclemr  7240  nnnninf2  7255  exmidonfinlem  7332  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  finacn  7347  exmidaclem  7351  exmidontriimlem3  7366  exmidontriimlem4  7367  exmidontriim  7368  iftrueb01  7369  pw1ne3  7376  sucpw1ne3  7378  sucpw1nel3  7379  onntri35  7383  acnccim  7419  elni2  7462  addnidpig  7484  elinp  7622  suplocexprlemdisj  7868  suplocexprlemub  7871  pitonn  7996  peano1nnnn  8000  peano2nnnn  8001  peano5nnnn  8040  sup3exmid  9065  peano5nni  9074  1nn  9082  peano2nn  9083  dfuzi  9518  uz11  9706  elfzonlteqm1  10376  frec2uzltd  10585  0tonninf  10622  1tonninf  10623  wrdsymb0  11063  lsw0  11078  swrdwrdsymbg  11155  sumeq1  11781  prodeq1f  11978  nninfctlemfo  12476  ctiunct  12926  ssomct  12931  issubm  13419  isnsg  13653  releqgg  13671  eqgex  13672  resghm  13711  ghmeql  13718  issubrg  14098  lmodfopnelem2  14202  islssm  14234  islssmg  14235  lspsneq0  14303  istopg  14586  fiinbas  14636  topbas  14654  epttop  14677  restbasg  14755  icnpimaex  14798  lmcvg  14804  iscnp4  14805  cncnpi  14815  cnconst2  14820  cnptoprest  14826  cnptoprest2  14827  cnpdis  14829  lmss  14833  lmff  14836  txbas  14845  eltx  14846  txcnp  14858  txlm  14866  blssps  15014  blss  15015  blssexps  15016  blssex  15017  neibl  15078  metss  15081  metrest  15093  xmettx  15097  metcnp3  15098  tgioo  15141  tgqioo  15142  uhgrm  15789  lpvtx  15790  incistruhgr  15801  umgrnloopvv  15825  uhgredgm  15842  uhgrvtxedgiedgb  15847  upgredg2vtx  15852  bdsep2  16021  bdzfauscl  16025  bj-indeq  16064  bj-nn0suc0  16085  bj-nnelirr  16088  bj-peano4  16090  bj-inf2vnlem2  16106  bj-nn0sucALT  16113  bj-findis  16114  strcollnft  16119  sscoll2  16123  2omap  16132  nninfsellemdc  16149  nninfsellemqall  16154  nnnninfex  16161