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  2702  rexeqf  2703  reueq1f  2704  rmoeq1f  2705  rabeqf  2767  clel3g  2915  clel4  2917  sbcbi2  3057  sbcel2gv  3070  csbeq2  3126  sbnfc2  3163  difeq2  3294  uneq1  3329  ineq1  3376  nel02  3474  n0i  3475  disjel  3524  exsnrex  3686  sneqr  3815  preqr1g  3821  preqr1  3823  preq12b  3825  prel12  3826  elunii  3870  eluniab  3877  ssuni  3887  elinti  3909  elintab  3911  intss1  3915  intmin  3920  intab  3929  iineq2  3959  dfiin2g  3975  breq  4062  axsep2  4180  zfauscl  4181  inuni  4216  exmidexmid  4257  ss1o0el1  4258  exmid01  4259  exmidundif  4267  exmidundifim  4268  rext  4278  intid  4287  mss  4289  opth1  4299  opeqex  4313  frforeq3  4413  frirrg  4416  limeq  4443  nsuceq0g  4484  suctr  4487  snnex  4514  uniuni  4517  iunpw  4546  ordtriexmidlem  4586  ordtriexmidlem2  4587  ordtriexmid  4588  ontriexmidim  4589  ordtri2orexmid  4590  ontr2exmid  4592  ordtri2or2exmidlem  4593  onsucelsucexmidlem  4596  onsucelsucexmid  4597  ordsucunielexmid  4598  regexmidlem1  4600  reg2exmidlema  4601  regexmid  4602  reg2exmid  4603  elirr  4608  en2lp  4621  suc11g  4624  dtruex  4626  ordsoexmid  4629  nlimsucg  4633  onintexmid  4640  reg3exmidlemwe  4646  reg3exmid  4647  peano5  4665  limom  4681  0elnn  4686  nn0eln0  4687  nnregexmid  4688  xpeq1  4708  xpeq2  4709  opthprc  4745  xp11m  5141  funopg  5325  dffo4  5753  funopdmsn  5789  elunirn  5860  f1oiso  5920  canth  5922  eusvobj2  5955  acexmidlema  5960  acexmidlemb  5961  acexmidlemab  5963  acexmidlem2  5966  mpoeq123  6029  oprssdmm  6282  unielxp  6285  cnvf1o  6336  smoel  6411  tfr0dm  6433  frecabcl  6510  nnsucelsuc  6602  nntri3or  6604  nntri2  6605  nntri3  6608  nndceq  6610  nnmordi  6627  nnaordex  6639  elqsn0m  6715  qsel  6724  mapsn  6802  en2m  6939  pw2f1odclem  6958  findcard2s  7015  undifdcss  7048  ctssdclemr  7242  nnnninf2  7257  exmidonfinlem  7334  exmidfodomrlemr  7343  exmidfodomrlemrALT  7344  finacn  7349  exmidaclem  7353  exmidontriimlem3  7368  exmidontriimlem4  7369  exmidontriim  7370  iftrueb01  7371  pw1ne3  7378  sucpw1ne3  7380  sucpw1nel3  7381  onntri35  7385  acnccim  7421  elni2  7464  addnidpig  7486  elinp  7624  suplocexprlemdisj  7870  suplocexprlemub  7873  pitonn  7998  peano1nnnn  8002  peano2nnnn  8003  peano5nnnn  8042  sup3exmid  9067  peano5nni  9076  1nn  9084  peano2nn  9085  dfuzi  9520  uz11  9708  elfzonlteqm1  10378  frec2uzltd  10587  0tonninf  10624  1tonninf  10625  wrdsymb0  11065  lsw0  11080  swrdwrdsymbg  11157  sumeq1  11827  prodeq1f  12024  nninfctlemfo  12522  ctiunct  12972  ssomct  12977  issubm  13465  isnsg  13699  releqgg  13717  eqgex  13718  resghm  13757  ghmeql  13764  issubrg  14144  lmodfopnelem2  14248  islssm  14280  islssmg  14281  lspsneq0  14349  istopg  14632  fiinbas  14682  topbas  14700  epttop  14723  restbasg  14801  icnpimaex  14844  lmcvg  14850  iscnp4  14851  cncnpi  14861  cnconst2  14866  cnptoprest  14872  cnptoprest2  14873  cnpdis  14875  lmss  14879  lmff  14882  txbas  14891  eltx  14892  txcnp  14904  txlm  14912  blssps  15060  blss  15061  blssexps  15062  blssex  15063  neibl  15124  metss  15127  metrest  15139  xmettx  15143  metcnp3  15144  tgioo  15187  tgqioo  15188  uhgrm  15835  lpvtx  15836  incistruhgr  15847  umgrnloopv  15871  uhgredgm  15891  uhgrvtxedgiedgb  15898  upgredg2vtx  15903  uhgr2edg  15961  bdsep2  16129  bdzfauscl  16133  bj-indeq  16172  bj-nn0suc0  16193  bj-nnelirr  16196  bj-peano4  16198  bj-inf2vnlem2  16214  bj-nn0sucALT  16221  bj-findis  16222  strcollnft  16227  sscoll2  16231  2omap  16240  nninfsellemdc  16257  nninfsellemqall  16262  nnnninfex  16269