Theorem eleq2 2269

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 2199	. . . . . 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 1581	. . . 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 1848	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2201	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2201	. 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 1515   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleq12  2270  eleq2i  2272  eleq2d  2275  nelneq2  2307  clelsb2  2311  dvelimdc  2369  nelne1  2466  neleq2  2476  raleqf  2698  rexeqf  2699  reueq1f  2700  rmoeq1f  2701  rabeqf  2762  clel3g  2907  clel4  2909  sbcbi2  3049  sbcel2gv  3062  csbeq2  3117  sbnfc2  3154  difeq2  3285  uneq1  3320  ineq1  3367  nel02  3465  n0i  3466  disjel  3515  exsnrex  3675  sneqr  3801  preqr1g  3807  preqr1  3809  preq12b  3811  prel12  3812  elunii  3855  eluniab  3862  ssuni  3872  elinti  3894  elintab  3896  intss1  3900  intmin  3905  intab  3914  iineq2  3944  dfiin2g  3960  breq  4047  axsep2  4164  zfauscl  4165  inuni  4200  exmidexmid  4241  ss1o0el1  4242  exmid01  4243  exmidundif  4251  exmidundifim  4252  rext  4260  intid  4269  mss  4271  opth1  4281  opeqex  4295  frforeq3  4395  frirrg  4398  limeq  4425  nsuceq0g  4466  suctr  4469  snnex  4496  uniuni  4499  iunpw  4528  ordtriexmidlem  4568  ordtriexmidlem2  4569  ordtriexmid  4570  ontriexmidim  4571  ordtri2orexmid  4572  ontr2exmid  4574  ordtri2or2exmidlem  4575  onsucelsucexmidlem  4578  onsucelsucexmid  4579  ordsucunielexmid  4580  regexmidlem1  4582  reg2exmidlema  4583  regexmid  4584  reg2exmid  4585  elirr  4590  en2lp  4603  suc11g  4606  dtruex  4608  ordsoexmid  4611  nlimsucg  4615  onintexmid  4622  reg3exmidlemwe  4628  reg3exmid  4629  peano5  4647  limom  4663  0elnn  4668  nn0eln0  4669  nnregexmid  4670  xpeq1  4690  xpeq2  4691  opthprc  4727  xp11m  5122  funopg  5306  dffo4  5730  funopdmsn  5766  elunirn  5837  f1oiso  5897  canth  5899  eusvobj2  5932  acexmidlema  5937  acexmidlemb  5938  acexmidlemab  5940  acexmidlem2  5943  mpoeq123  6006  oprssdmm  6259  unielxp  6262  cnvf1o  6313  smoel  6388  tfr0dm  6410  frecabcl  6487  nnsucelsuc  6579  nntri3or  6581  nntri2  6582  nntri3  6585  nndceq  6587  nnmordi  6604  nnaordex  6616  elqsn0m  6692  qsel  6701  mapsn  6779  pw2f1odclem  6933  findcard2s  6989  undifdcss  7022  ctssdclemr  7216  nnnninf2  7231  exmidonfinlem  7303  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  finacn  7318  exmidaclem  7322  exmidontriimlem3  7337  exmidontriimlem4  7338  exmidontriim  7339  pw1ne3  7344  sucpw1ne3  7346  sucpw1nel3  7347  onntri35  7351  acnccim  7386  elni2  7429  addnidpig  7451  elinp  7589  suplocexprlemdisj  7835  suplocexprlemub  7838  pitonn  7963  peano1nnnn  7967  peano2nnnn  7968  peano5nnnn  8007  sup3exmid  9032  peano5nni  9041  1nn  9049  peano2nn  9050  dfuzi  9485  uz11  9673  elfzonlteqm1  10341  frec2uzltd  10550  0tonninf  10587  1tonninf  10588  wrdsymb0  11028  lsw0  11043  swrdwrdsymbg  11120  sumeq1  11699  prodeq1f  11896  nninfctlemfo  12394  ctiunct  12844  ssomct  12849  issubm  13337  isnsg  13571  releqgg  13589  eqgex  13590  resghm  13629  ghmeql  13636  issubrg  14016  lmodfopnelem2  14120  islssm  14152  islssmg  14153  lspsneq0  14221  istopg  14504  fiinbas  14554  topbas  14572  epttop  14595  restbasg  14673  icnpimaex  14716  lmcvg  14722  iscnp4  14723  cncnpi  14733  cnconst2  14738  cnptoprest  14744  cnptoprest2  14745  cnpdis  14747  lmss  14751  lmff  14754  txbas  14763  eltx  14764  txcnp  14776  txlm  14784  blssps  14932  blss  14933  blssexps  14934  blssex  14935  neibl  14996  metss  14999  metrest  15011  xmettx  15015  metcnp3  15016  tgioo  15059  tgqioo  15060  bdsep2  15859  bdzfauscl  15863  bj-indeq  15902  bj-nn0suc0  15923  bj-nnelirr  15926  bj-peano4  15928  bj-inf2vnlem2  15944  bj-nn0sucALT  15951  bj-findis  15952  strcollnft  15957  sscoll2  15961  2omap  15969  nninfsellemdc  15984  nninfsellemqall  15989  nnnninfex  15996