Theorem eleq2 2230

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 2159	. . . . . 6 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
2	1	biimpi 119	. . . . 5 |- ( A = B -> A. x ( x e. A <-> x e. B ) )
3	2	19.21bi 1546	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
4	3	anbi2d 460	. . 3 |- ( A = B -> ( ( x = C /\ x e. A ) <-> ( x = C /\ x e. B ) ) )
5	4	exbidv 1813	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2161	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2161	. 2 |- ( C e. B <-> E. x ( x = C /\ x e. B ) )
8	5, 6, 7	3bitr4g 222	1 |- ( A = B -> ( C e. A <-> C e. B ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1341   = wceq 1343   E.wex 1480   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eleq12  2231  eleq2i  2233  eleq2d  2236  nelneq2  2268  clelsb2  2272  dvelimdc  2329  nelne1  2426  neleq2  2436  raleqf  2657  rexeqf  2658  reueq1f  2659  rmoeq1f  2660  rabeqf  2716  clel3g  2860  clel4  2862  sbcbi2  3001  sbcel2gv  3014  csbeq2  3069  sbnfc2  3105  difeq2  3234  uneq1  3269  ineq1  3316  n0i  3414  disjel  3463  exsnrex  3618  sneqr  3740  preqr1g  3746  preqr1  3748  preq12b  3750  prel12  3751  elunii  3794  eluniab  3801  ssuni  3811  elinti  3833  elintab  3835  intss1  3839  intmin  3844  intab  3853  iineq2  3883  dfiin2g  3899  breq  3984  axsep2  4101  zfauscl  4102  inuni  4134  exmidexmid  4175  ss1o0el1  4176  exmid01  4177  exmidundif  4185  exmidundifim  4186  rext  4193  intid  4202  mss  4204  opth1  4214  opeqex  4227  frforeq3  4325  frirrg  4328  limeq  4355  nsuceq0g  4396  suctr  4399  snnex  4426  uniuni  4429  iunpw  4458  ordtriexmidlem  4496  ordtriexmidlem2  4497  ordtriexmid  4498  ontriexmidim  4499  ordtri2orexmid  4500  ontr2exmid  4502  ordtri2or2exmidlem  4503  onsucelsucexmidlem  4506  onsucelsucexmid  4507  ordsucunielexmid  4508  regexmidlem1  4510  reg2exmidlema  4511  regexmid  4512  reg2exmid  4513  elirr  4518  en2lp  4531  suc11g  4534  dtruex  4536  ordsoexmid  4539  nlimsucg  4543  onintexmid  4550  reg3exmidlemwe  4556  reg3exmid  4557  peano5  4575  limom  4591  0elnn  4596  nn0eln0  4597  nnregexmid  4598  xpeq1  4618  xpeq2  4619  opthprc  4655  xp11m  5042  funopg  5222  dffo4  5633  elunirn  5734  f1oiso  5794  canth  5796  eusvobj2  5828  acexmidlema  5833  acexmidlemb  5834  acexmidlemab  5836  acexmidlem2  5839  mpoeq123  5901  oprssdmm  6139  unielxp  6142  cnvf1o  6193  smoel  6268  tfr0dm  6290  frecabcl  6367  nnsucelsuc  6459  nntri3or  6461  nntri2  6462  nntri3  6465  nndceq  6467  nnmordi  6484  nnaordex  6495  elqsn0m  6569  qsel  6578  mapsn  6656  findcard2s  6856  undifdcss  6888  ctssdclemr  7077  nnnninf2  7091  exmidonfinlem  7149  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  exmidontriimlem3  7179  exmidontriimlem4  7180  exmidontriim  7181  pw1ne3  7186  sucpw1ne3  7188  sucpw1nel3  7189  onntri35  7193  elni2  7255  addnidpig  7277  elinp  7415  suplocexprlemdisj  7661  suplocexprlemub  7664  pitonn  7789  peano1nnnn  7793  peano2nnnn  7794  peano5nnnn  7833  sup3exmid  8852  peano5nni  8860  1nn  8868  peano2nn  8869  dfuzi  9301  uz11  9488  elfzonlteqm1  10145  frec2uzltd  10338  0tonninf  10374  1tonninf  10375  sumeq1  11296  prodeq1f  11493  ctiunct  12373  ssomct  12378  istopg  12647  fiinbas  12697  topbas  12717  epttop  12740  restbasg  12818  icnpimaex  12861  lmcvg  12867  iscnp4  12868  cncnpi  12878  cnconst2  12883  cnptoprest  12889  cnptoprest2  12890  cnpdis  12892  lmss  12896  lmff  12899  txbas  12908  eltx  12909  txcnp  12921  txlm  12929  blssps  13077  blss  13078  blssexps  13079  blssex  13080  neibl  13141  metss  13144  metrest  13156  xmettx  13160  metcnp3  13161  tgioo  13196  tgqioo  13197  bdsep2  13778  bdzfauscl  13782  bj-indeq  13821  bj-nn0suc0  13842  bj-nnelirr  13845  bj-peano4  13847  bj-inf2vnlem2  13863  bj-nn0sucALT  13870  bj-findis  13871  strcollnft  13876  sscoll2  13880  nninfsellemdc  13900  nninfsellemqall  13905