Theorem ineq1 2262

Description: Equality theorem for intersection of two classes.

Assertion

Ref	Expression
ineq1	⊢ (A = B → (A ∩ C) = (B ∩ C))

Proof of Theorem ineq1

Step	Hyp	Ref	Expression
1		eleq2 1578	. . . 4 ⊢ (A = B → (x ∈ A ↔ x ∈ B))
2	1	anbi1d 620	. . 3 ⊢ (A = B → ((x ∈ A ⋀ x ∈ C) ↔ (x ∈ B ⋀ x ∈ C)))
3		elin 2259	. . 3 ⊢ (x ∈ (A ∩ C) ↔ (x ∈ A ⋀ x ∈ C))
4		elin 2259	. . 3 ⊢ (x ∈ (B ∩ C) ↔ (x ∈ B ⋀ x ∈ C))
5	2, 3, 4	3bitr4g 558	. 2 ⊢ (A = B → (x ∈ (A ∩ C) ↔ x ∈ (B ∩ C)))
6	5	eqrdv 1516	1 ⊢ (A = B → (A ∩ C) = (B ∩ C))

Syntax hints:   → wi 3   ⋀ wa 221   = wceq 992   ∈ wcel 994   ∩ cin 2098

This theorem is referenced by:  ineq2 2263  ineq12 2264  ineq1i 2265  ineq1d 2268  unineq 2307  inex1g 2792  frc 2950  onnev 3329  reseq1 3455  isofrlem 4015  fiint 4703  inf3lema 4754  aceq5lem5 4885  kmlem12 4922  kmlem14 4924  cdaung 5073  inopn 7812  isbasisg 7823  basis1 7826  basis2 7827  tgval 7828  subtop 7858  cctop 7862  elcls 7914  clsndisj 7916  elcls3 7921  islp2 7957  lpbl 8090  methausi 8092  omlsi 9522  pjoml 9545  shincl 9627  shmodi 9639  chm0 9690  chincl 9698  chdmm1 9724  ledi 9739  cmbr 9803  cmbr3 9827  mdbr 10502  dmdmd 10508  dmdi 10510  dmdbr3 10513  dmdbr4 10514  mdslmd1lem4 10536  cvmd 10544  cvexch 10582  dmdbr6ati 10632  mddmdin0i 10640  infi1 10735  intprd 10755  neiopne 10757  subspemp 11060  sbtpsines 11062  filint 11075  cnfilca 11088  dtt2 11110  bwt2 11123  elfiun 11421  fictblem 11422  fictb 11423  opnbnd 11461  hausnei2 11471  elsubsp 11477  subspid 11478  subsubtop 11479  subcld 11480  subcls 11481  compsublem 11487  compsub 11488  hscptsscld 11491  dfcon2 11501  connsub 11502  reconnlem1 11507  isfne 11541  locfincomp 11575  neibastop1 11579  nrmsep 11615  nrmsep2 11616  isfbas 11621  fbasssin 11625  fbunfip 11631  fgf 11632  isufil2 11650  filcon 11665  fclusnei 11719  fclusneii 11721  fcluscf 11724  flimfnfcls 11727  fclusfnei 11738  fclsfneii 11740  tailfb 11762  inficl 11849  subspopn 11900  subspcld 11901  subspabs 11903  metsstop 11909  icoopnst 11940  iocopnst 11941  cnres 11950  cnss 11953  txbas 11973  txsubsp 11983  sstotbnd 11992  totbndss 11993  bndss 11998  ishgrag 12195  hgralem 12196  ispgrag 12205

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-in 2103

Copyright terms: Public domain