Theorem eleq2 1535

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 1470	. . . . . 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 1060	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	anbi2d 616	. . 3 |- (A = B -> ((x = C /\ x e. A) <-> (x = C /\ x e. B)))
5	4	exbidv 1279	. 2 |- (A = B -> (E.x(x = C /\ x e. A) <-> E.x(x = C /\ x e. B)))
6		df-clel 1472	. 2 |- (C e. A <-> E.x(x = C /\ x e. A))
7		df-clel 1472	. 2 |- (C e. B <-> E.x(x = C /\ x e. B))
8	5, 6, 7	3bitr4g 555	1 |- (A = B -> (C e. A <-> C e. B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 954   = wceq 956   e. wcel 958  E.wex 980

This theorem is referenced by:  eleq12 1536  eleq2i 1538  eleq2d 1541  nelneq2 1562  neleq2 1643  raleq1f 1783  rexeq1f 1784  reueq1f 1785  rabeqf 1808  clel3g 1892  clel4 1894  sbcel2gv 1981  csbiegft 2029  difeq1 2153  difeq2 2154  uneq1 2177  ineq1 2210  unineq 2255  n0i 2285  rzal 2355  ifeq1 2364  ifeq2 2365  elif 2378  disjsn 2441  sneqr 2477  preqr1 2481  preq12b 2483  prel12 2484  elunii 2508  unieq 2510  eluniab 2513  elinti 2542  elintab 2544  intss1 2548  intmin 2553  intab 2560  iineq2 2579  iununi 2616  breq 2621  trel 2687  zfrepclf 2699  zfauscl 2705  el 2751  rext 2754  unipw 2756  opth1 2786  opprc3 2797  opeqex 2798  opthwiener 2807  epelc 2833  uniuni 2880  euuni 2881  reucl 2885  iunpw 2914  efrirr 2928  ordtri1 2980  ordtri3 2983  oneqmin 3018  onminex 3020  nsuceq0 3053  ordnbtwn 3063  onsucuni2 3091  onuninsuc 3108  limomss 3137  nnlim 3144  peano5 3153  xpeq1 3200  xpeq2 3201  opthprc 3221  0nelxp 3240  onxpdisj 3241  funopg 3547  fn0 3605  fv3 3733  dffo4 3820  elunirnALT 3869  f1oiso 3904  canth 3907  tz7.48lem 3955  ndmoprg 4043  unielxp 4107  oawordeulem 4188  oaordex 4192  oarec 4196  omordi 4197  oneo 4212  oeordi 4214  omsmolem 4256  erth 4282  mapsn 4345  pw2en 4446  pssnn 4534  unfilem3 4550  abfii4OLD 4564  zfregcl 4595  elirr 4599  en2lp 4602  suc11reg 4605  inf0 4606  inf3lem2 4614  inf3lem3 4615  infeq5 4621  axinf2 4624  dfom3 4630  elom3 4631  noinfep 4640  r1ord 4655  r1val1 4658  rankr1 4674  rankval3 4681  rankuni2 4690  rankun 4691  aceq1 4729  aceq2 4731  aceq3 4733  aceq5lem2 4736  aceq5lem4 4738  aceq6a 4741  aceq6b 4742  kmlem2 4766  kmlem4 4768  zorn2lem7 4794  brdom7disj 4804  brdom6disj 4805  unidom 4808  cardlim 4851  alephnbtwn 4868  alephordi 4874  cardaleph 4885  alephfp 4900  alephval3 4903  axpowndlem3 4951  ltpiord 5015  addnidpi 5028  indpi 5034  elnp 5092  genpnnp 5108  1pr 5117  ltaddpr 5140  peano5nn 5926  dfnn2 5936  dfuz 6202  peano5uz 6203  om2uzlt 6298  eliooret 6386  uz11t 6432  fzoptht 6502  istopg 7596  topbast 7627  bastop 7642  subbasOLD 7644  retopbas 7655  clsval2 7685  elcls 7704  clsndisj 7706  elcls3 7711  islp2 7747  qdensere 7751  cnfval 7756  cnpimaex 7765  cnsscnp 7772  blex 7849  blss 7853  blssex 7854  opnm 7860  opnin 7869  neibl 7877  methausi 7881  metcnp 7887  tgioo 7915  bcthlem29 8027  sh 9078  closedsub 9093  pjtheut 9236  pjmvalt 9238  pjoc1t 9267  h1dn0 9475  spansneleqi 9492  nonbool 9596  pjcht 9639  pjnelt 9671  cdjreu 10359  ntunte 10439  uninqs 10441  elioo1t3 10496  homeofval 10516  hmeogrp 10538  isfil 10558  rcfpfillem3 10589  rcfpfillem3OLD 10590  dtt2 10618

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain