Theorem eleq2 1578

Description: Equality implies equivalence of membership.

Assertion

Ref	Expression
eleq2	|- (A = B -> (C e. A <-> C e. B))

Proof of Theorem eleq2

Step	Hyp	Ref	Expression
1		dfcleq 1512	. . . . . 6 |- (A = B <-> A.x(x e. A <-> x e. B))
2	1	biimpi 149	. . . . 5 |- (A = B -> A.x(x e. A <-> x e. B))
3	2	19.21bi 1096	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	anbi2d 619	. . 3 |- (A = B -> ((x = C /\ x e. A) <-> (x = C /\ x e. B)))
5	4	exbidv 1317	. 2 |- (A = B -> (E.x(x = C /\ x e. A) <-> E.x(x = C /\ x e. B)))
6		df-clel 1514	. 2 |- (C e. A <-> E.x(x = C /\ x e. A))
7		df-clel 1514	. 2 |- (C e. B <-> E.x(x = C /\ x e. B))
8	5, 6, 7	3bitr4g 558	1 |- (A = B -> (C e. A <-> C e. B))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221  A.wal 990   = wceq 992   e. wcel 994  E.wex 1016

This theorem is referenced by:  eleq12 1579  eleq2i 1581  eleq2d 1584  nelneq2 1605  neleq2 1689  raleq1f 1829  rexeq1f 1830  reueq1f 1831  rabeqf 1854  clel3g 1938  clel4 1940  sbcel2gv 2029  csbiegft 2081  difeq1 2205  difeq2 2206  uneq1 2229  ineq1 2262  unineq 2307  n0i 2337  rzal 2409  ifeq1 2418  ifeq2 2419  elif 2432  disjsn 2502  sneqr 2542  preqr1 2546  preq12b 2548  prel12 2549  elunii 2574  unieq 2576  eluniab 2579  reucl 2584  elinti 2609  elintab 2611  intss1 2615  intmin 2620  intab 2627  iineq2 2647  iununi 2686  breq 2694  trel 2761  zfrepclf 2773  zfauscl 2779  elALT 2827  rext 2834  intid 2843  opth1 2862  opprc3 2873  opeqex 2874  opthwiener 2884  epelc 2911  efrirr 2957  ordtri1 3008  ordtri3 3011  nsuceq0 3053  suctr 3055  ordnbtwn 3062  snnex 3100  uniuni 3104  euuni 3105  iunpw 3137  oneqmin 3162  onminex 3164  onsucuni2 3188  onuninsuci 3194  limomss 3224  nnlim 3231  peano5 3241  xpeq1 3281  xpeq2 3282  opthprc 3306  0nelxp 3326  0nelelxp 3327  onxpdisj 3328  funopg 3652  fn0 3711  fv3 3844  dffo4 3934  elunirnALT 3983  f1oiso 4018  ndmoprg 4104  unielxp 4167  canth 4205  tz7.48lem 4256  oawordeulem 4324  oaordex 4328  oarec 4332  omordi 4333  oneo 4348  oeordi 4350  oeoa 4360  oeoe 4362  omsmolem 4396  erth 4422  uniqs 4436  mapsn 4486  pw2en 4587  pssnn 4681  unfilem3 4696  abfii4 4707  zfregcl 4738  elirr 4742  en2lp 4747  suc11reg 4750  inf0 4751  inf3lem2 4759  inf3lem3 4760  infeq5 4766  axinf2 4769  dfom3 4776  elom3 4777  noinfep 4786  r1ord 4801  r1val1 4804  rankr1 4820  rankval3 4827  rankuni2 4836  rankun 4837  aceq1 4875  aceq2 4877  aceq3 4879  aceq5lem2 4882  aceq5lem4 4884  aceq6a 4887  aceq6b 4888  kmlem2 4912  kmlem4 4914  zorn2lem7 4940  brdom7disj 4950  brdom6disj 4951  unidom 4954  cardlim 5001  alephnbtwn 5018  alephordi 5024  cardaleph 5035  alephfp 5050  alephval3 5053  axpowndlem3 5105  ltpiord 5169  addnidpi 5182  indpi 5188  elnp 5246  genpnnp 5262  1pr 5271  ltaddpr 5294  peano5nni 6071  dfnn2 6081  dfuzi 6373  peano5uzi 6374  elioore 6512  uz11 6559  fzopth 6632  om2uzlti 6661  istopg 7808  topbas 7839  bastop1 7854  subbas 7856  retopbas 7865  clsval2 7895  elcls 7914  clsndisj 7916  elcls3 7921  islp2 7957  qdensere 7961  cnfval 7966  cnpimaex 7975  cnsscnp 7982  blex 8059  blss 8063  blssex 8064  opnm 8070  opnin 8079  neibl 8087  methausi 8092  metcnp 8098  tgioo 8126  bcthlem29 8238  sh 9354  closedsub 9369  pjtheu 9512  pjmval 9514  pjoc1 9543  h1dn0 9751  spansneleqi 9768  nonbooli 9874  pjch 9917  pjnel 9949  cdjreui 10641  ntunte 10728  uninqs 10730  domintreflem 10766  isexid2 10901  unmnd 10951  uznzr 10967  elioo1t3 10996  nsn 11017  homeofval 11022  hmeogrp 11044  isfil 11071  rcfpfillem3 11091  dtt2 11110  bwt2 11123  usinuniop 11128  altretoplem2 11143  altretop 11144  extrdom 11236  extrcod 11237  extrcmp 11238  extrid 11239  dfiin2g 11400  lpni 11417  fictb 11423  ordtypelem5 11431  hartoglem 11435  infenomsub 11450  subntr 11482  compsublem 11487  compsub 11488  cptclsscpt 11489  hscptsscld 11491  alexsublem3 11498  alexsub 11500  subtopmetlem 11505  subtopmet 11506  2ndc1stc 11538  2ndcctbss 11539  isfne3 11543  fneint 11547  fness 11552  fneref 11554  topfneec2 11563  locfindsc 11576  comppfsc 11578  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  ist1-2 11603  ist1-3 11604  extbas1 11641  isufil 11649  isufil2 11650  filssufillem 11655  fixufil 11661  ufinffr 11663  flimopn 11679  limfilcf 11683  flimcls 11684  rnelfm 11699  fclusnei 11719  fcluscf 11724  flimfnfcls 11727  fclusfnei 11738  tailuni 11761  filnetlem1 11763  filnetlem2 11764  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  filnet 11768  dif1card 11835  fimax 11837  acdc3g 11843  acdc5g 11844  indexf 11847  fiinbas 11905  metsstop 11909  haustlmu 11967  lmtlm 11969  sstotbnd 11992  totbndss 11993  isbnd3 11997  totbndbnd 12000  ismtyhmeolem 12006  ismtybndlem 12008  heiborlem1 12011  heiborlem28 12038  heiborlem30 12040  heiborlem31 12041  rrntotbnd 12078  ssunipwALT 12211

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-cleq 1511  df-clel 1514

Copyright terms: Public domain