Theorem eleq2 1958

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 1878	. . . . . 6 |- (A = B <-> A.x(x e. A <-> x e. B))
2	1	biimpi 168	. . . . 5 |- (A = B -> A.x(x e. A <-> x e. B))
3	2	19.21bi 1408	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	anbi2d 678	. . 3 |- (A = B -> ((x = C /\ x e. A) <-> (x = C /\ x e. B)))
5	4	exbidv 1657	. 2 |- (A = B -> (E.x(x = C /\ x e. A) <-> E.x(x = C /\ x e. B)))
6		df-clel 1880	. 2 |- (C e. A <-> E.x(x = C /\ x e. A))
7		df-clel 1880	. 2 |- (C e. B <-> E.x(x = C /\ x e. B))
8	5, 6, 7	3bitr4g 614	1 |- (A = B -> (C e. A <-> C e. B))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326

This theorem is referenced by:  eleq12 1959  eleq2i 1961  eleq2d 1964  nelneq2 1986  nelne 2100  neleq2 2102  raleqf 2263  rexeqf 2264  reueq1f 2265  rabeqf 2288  clel3g 2397  clel4 2399  sbcel2gv 2512  sbcel2gvOLD 2513  csbiegft 2573  difeq1OLD 2718  difeq2 2719  difeq2OLD 2720  uneq1 2748  ineq1 2789  unineq 2844  n0i 2880  rzalOLD 2971  ifeq1 2985  ifeq1OLD 2986  ifeq2 2987  ifeq2OLD 2988  elif 3005  disjsnOLD 3090  sneqr 3147  preqr1 3152  preq12b 3154  prel12 3155  elunii 3182  unieqOLD 3186  eluniab 3189  ssuni 3201  reucl 3213  elinti 3223  elintiOLD 3224  elintab 3227  intss1 3231  intmin 3237  intminOLD 3238  intab 3247  iineq2 3274  iineq2OLD 3275  dfiin2g 3286  iununi 3331  iununiOLD 3332  breq 3340  trelOLD 3419  zfrepclf 3434  zfauscl 3440  inuni 3470  elALT 3494  rext 3502  intid 3512  opth1 3531  opprc3 3543  opeqex 3544  opthwiener 3554  epelc 3584  efrirr 3637  ordtri1 3693  ordtri1OLD 3694  ordtri3 3697  ordtri3OLD 3698  nsuceq0 3749  suctr 3751  trsuc2 3754  ordnbtwn 3761  snnex 3801  uniuni 3806  euuni 3807  iunpw 3858  oneqmin 3886  onminex 3888  onsucuni2OLD 3915  onuninsuci 3921  nlimsucg 3923  limomss 3956  nnlim 3964  peano5 3975  xpeq1 4016  xpeq2 4017  opthprc 4046  0nelxp 4066  0nelelxp 4067  onxpdisjOLD 4069  funopg 4454  fn0OLD 4533  fv3 4690  nfunsnOLD 4707  dffv2 4734  dffo4 4793  elunirnALT 4845  f1oiso 4881  ndmoprg 4976  unielxp 5047  canth 5112  tz7.48lem 5164  oawordeulem 5236  oaordex 5240  oarec 5244  omordi 5245  oneo 5260  oeordi 5262  oeoa 5272  oeoe 5274  omsmolem 5313  erth 5340  uniqs 5354  mapsn 5404  pw2en 5505  pssnn 5628  unfilem3 5643  abfii4 5654  ordtypelem5 5688  hartoglem 5692  zfregcl 5697  elirrOLD 5702  en2lp 5707  suc11reg 5710  inf0 5712  inf3lem2 5720  inf3lem3 5721  infeq5 5727  axinf2 5730  dfom3 5737  elom3 5738  noinfep 5747  en3lplem1 5756  en3lp 5758  r1ord 5766  r1val1 5769  rankr1 5785  rankval3 5792  rankuni2 5801  rankun 5802  tratrb 5831  infenomsub 5889  aceq1 5891  aceq2 5893  aceq3 5895  aceq5lem2 5898  aceq5lem4 5900  aceq6a 5903  aceq6b 5904  kmlem2 5928  kmlem4 5930  zorn2lem7 5956  brdom7disj 5966  brdom6disj 5967  unidom 5970  cardlim 6003  alephnbtwn 6016  alephordi 6022  cardaleph 6033  alephfp 6048  alephval3 6051  axpowndlem3 6103  ltpiord 6167  addnidpi 6180  indpi 6186  elnp 6244  genpnnp 6260  1pr 6269  ltaddpr 6292  peano5nni 7109  dfnn2 7119  dfuzi 7414  peano5uzi 7415  elioore 7554  uz11 7601  fzopth 7674  om2uzlti 7709  istopg 8865  fiinbas 8885  topbas 8897  bastop1 8912  subbas 8914  retopbas 8925  clsval2 8961  elcls 8980  clsndisj 8982  elcls3 8987  islp2 9023  qdensere 9027  cnfval 9032  cnpimaex 9041  cnsscnp 9049  blex 9126  blss 9130  blssex 9131  opnm 9137  opnin 9146  neibl 9154  methausi 9159  metcnp 9165  tgioo 9193  bcthlem29 9305  indexfi 10174  dif1card 10177  homeofval 10234  subtopmetlem 10255  subtopmet 10256  isfil 10266  extbas1 10291  flimopn 10321  usinuniop 10341  lpni 10347  isexid2 10372  unmnd 10405  uznzr 10416  sh 10711  closedsub 10726  pjtheu 10869  pjmval 10871  pjoc1 10900  h1dn0 11108  spansneleqi 11125  nonbooli 11231  pjch 11274  pjnel 11306  cdjreui 12004  bnj143 12475  bnj216 12507  bnj530 12527  bnj531 12528  bnj532 12529  bnj533 12530  bnj957 12852  bnj1063 12899  bnj1337 13064  bnj1343 13067  bnj517 13259  bnj916 13332  bnj983 13357  bnj1001 13366  bnj1145 13431  bnj1154 13438  bnj1498 13562  trsuc2OLD 13793  untelirr 13796  untsucf 13798  epelcNEW 13826  epelg 13827  dfon2lem4 13852  dfon2lem7 13855  dfon2lem9 13857  dford4lem2 13860  ordsucuniel 13863  soseq 13955  axdenselem8 14026  nocvxminlem 14028  uninqs 14340  fvsnn 14450  injrec 14461  surjsec 14462  ispr1 14496  repcpwti 14503  isprj1 14505  unprj 14511  prl2 14514  preoref22 14570  supdef 14604  defse3 14614  dutos1 14626  ablcomgrp 14702  clfsebs2 14710  fprodneg 14741  fprodsub 14742  elioo1t3 14846  nsn 14874  hmeogrp 14892  stoig2b 14906  prtoptop 14919  rcfpfillem3 14930  fbaslim2 14936  limvinlv 14941  dtt2 14951  bwt2 14960  trhom 14983  altretoplem2 14996  altretop 14997  dualded 15132  dualcat2 15133  tarval 15212  tarvalg 15213  tarval1 15214  tarval1g 15215  bpmp 15251  btmp 15252  cardtar 15281  elcarelcl 15283  isline1 15294  isseg1 15304  isplibg1 15309  isplibg2 15311  isplibg3 15313  isplibg4a 15315  isplibg4b 15317  dfiin2gOLD 15356  fictb 15371  ordtypelem5OLD 15379  hartoglemOLD 15383  infenomsubOLD 15398  subntr 15425  compsublem 15430  compsub 15431  cptclsscpt 15432  hscptsscld 15434  alexsublem3 15439  alexsub 15441  2ndc1stc 15477  2ndcctbss 15478  isfne3 15482  fneint 15486  fness 15491  fneref 15493  topfneec2 15502  locfindsc 15515  comppfsc 15517  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  ist1-2 15542  ist1-3 15543  isufil 15564  isufil2 15565  filssufillem 15570  fixufil 15576  ufinffr 15578  limfilcf 15587  flimcls 15588  rnelfm 15593  fclusnei 15607  fcluscf 15612  flimfnfcls 15615  fclusfnei 15626  tailuni 15638  filnetlem1 15640  filnetlem2 15641  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  filnet 15645  cover2 15673  fimax 15746  acdc3g 15751  acdc5g 15752  indexfiOLD 15755  haustlmu 15906  lmtlm 15908  txmet 15925  sstotbnd 15936  totbndss 15937  isbnd3 15941  totbndbnd 15944  ismtyhmeolem 15950  ismtybndlem 15952  heiborlem1 15955  heiborlem28 15982  heiborlem30 15984  heiborlem31 15985  rrntotbnd 16022  grpkerinj 16042  isidl 16162  1idl 16174  0ring 16175  ispridl 16182  smprngpr 16200  isfldidl 16216  isdmn3 16222  prtlem10 16265  0nelqs2 16269  prter3 16286  smoel 16451  suctrALT2VD 16660  suctrALT2 16661  en3lplem1VD 16667  en3lpVD 16669  tratrbVD 16685  isgrpNEW 17104  isringNEW 17142  issrng 17176  islvec 17188  isphil 17195  ispsubsp 17226  pointpsub 17231  linepsub 17232

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-cleq 1877  df-clel 1880

Copyright terms: Public domain