Theorem eleq2 1527

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 1463	. . . . . 6 |- (A = B <-> A.x(x e. A <-> x e. B))
2	1	biimp 151	. . . . 5 |- (A = B -> A.x(x e. A <-> x e. B))
3	2	19.21bi 1056	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	anbi2d 614	. . 3 |- (A = B -> ((x = C /\ x e. A) <-> (x = C /\ x e. B)))
5	4	exbidv 1274	. 2 |- (A = B -> (E.x(x = C /\ x e. A) <-> E.x(x = C /\ x e. B)))
6		df-clel 1465	. 2 |- (C e. A <-> E.x(x = C /\ x e. A))
7		df-clel 1465	. 2 |- (C e. B <-> E.x(x = C /\ x e. B))
8	5, 6, 7	3bitr4g 553	1 |- (A = B -> (C e. A <-> C e. B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 951   = wceq 953   e. wcel 955  E.wex 977

This theorem is referenced by:  eleq12 1528  eleq2i 1530  eleq2d 1533  nelneq2 1554  neleq2 1635  raleq1f 1775  rexeq1f 1776  reueq1f 1777  rabeqf 1799  clel3g 1883  clel4 1885  sbcel2gv 1971  csbiegft 2019  difeq1 2143  difeq2 2144  uneq1 2167  ineq1 2200  unineq 2245  n0i 2275  rzal 2345  ifeq1 2354  ifeq2 2355  elif 2368  disjsn 2431  sneqr 2468  preqr1 2472  preq12b 2474  prel12 2475  elunii 2498  unieq 2500  eluniab 2503  elinti 2532  elintab 2534  intss1 2538  intmin 2543  intab 2550  iineq2 2569  iununi 2606  breq 2611  trel 2677  zfrepclf 2689  zfauscl 2695  el 2741  rext 2744  unipw 2746  opth1 2776  opprc3 2787  opth1gOLD 2788  opthwiener 2796  epelc 2822  uniuni 2870  euuni 2871  reucl 2875  iunpw 2904  efrirr 2918  ordtri1 2970  ordtri3 2973  oneqmin 3008  onminex 3010  nsuceq0 3043  ordnbtwn 3053  onsucuni2 3081  onuninsuc 3098  limomss 3127  nnlim 3134  peano5 3143  xpeq1 3190  xpeq2 3191  opthprc 3211  0nelxp 3230  onxpdisj 3231  funopg 3533  fn0 3591  fv3 3718  dffo4 3805  elunirnALT 3854  f1oiso 3889  canth 3892  tz7.48lem 3940  ndmoprg 4028  unielxp 4091  oawordeulem 4172  oaordex 4176  oarec 4180  omordi 4181  oneo 4196  oeordi 4198  omsmolem 4240  erth 4266  mapsn 4329  pw2en 4426  pssnn 4513  unfilem3 4526  abfii4 4538  zfregcl 4567  elirr 4571  en2lp 4574  suc11reg 4577  inf0 4578  inf3lem2 4586  inf3lem3 4587  infeq5 4593  axinf2 4596  dfom3 4602  elom3 4603  noinfep 4612  r1ord 4627  r1val1 4630  rankr1 4646  rankval3 4653  rankuni2 4662  rankun 4663  aceq1 4701  aceq2 4703  aceq3 4705  aceq5lem2 4708  aceq5lem4 4710  aceq6a 4713  aceq6b 4714  kmlem2 4738  kmlem4 4740  zorn2lem7 4766  brdom7disj 4776  brdom6disj 4777  unidom 4780  cardlim 4823  alephnbtwn 4840  alephordi 4846  cardaleph 4857  alephfp 4872  alephval3 4875  axpowndlem3 4923  ltpiord 4987  addnidpi 5000  indpi 5006  elnp 5064  genpnnp 5080  1pr 5089  ltaddpr 5112  peano5nn 5874  dfnn2 5884  dfuz 6150  peano5uz 6151  om2uzlt 6235  uz11t 6364  fzoptht 6434  istopg 7538  topbast 7569  bastop 7584  subbas 7586  retopbas 7597  clsval2 7627  elcls 7646  clsndisj 7648  elcls3 7652  islp2 7688  qdensere 7691  cnfval 7696  cnpimaex 7704  cnsscnp 7711  blex 7789  blss 7793  blssex 7794  opnm 7800  opnin 7809  neibl 7817  methausi 7820  metcnp 7826  tgioo 7854  bcthlem29 7961  sh 8999  closedsub 9014  pjtheut 9151  pjmvalt 9153  pjoc1t 9182  h1dn0 9390  spansneleqi 9408  nonbool 9513  pjcht 9556  pjnelt 9588  cdjreu 10264  ntunte 10340  uninqs 10342  elioo1t3 10383  homeofval 10403  hmeogrp 10425  isfil 10433  dtt2 10462

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465

Copyright terms: Public domain