Theorem ineq1 2213

Description: Equality theorem for intersection of two classes.

Assertion

Ref	Expression
ineq1	|- (A = B -> (A i^i C) = (B i^i C))

Proof of Theorem ineq1

Step	Hyp	Ref	Expression
1		eleq2 1538	. . . 4 |- (A = B -> (x e. A <-> x e. B))
2	1	anbi1d 619	. . 3 |- (A = B -> ((x e. A /\ x e. C) <-> (x e. B /\ x e. C)))
3		elin 2210	. . 3 |- (x e. (A i^i C) <-> (x e. A /\ x e. C))
4		elin 2210	. . 3 |- (x e. (B i^i C) <-> (x e. B /\ x e. C))
5	2, 3, 4	3bitr4g 557	. 2 |- (A = B -> (x e. (A i^i C) <-> x e. (B i^i C)))
6	5	eqrdv 1476	1 |- (A = B -> (A i^i C) = (B i^i C))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 958   e. wcel 960   i^i cin 2049

This theorem is referenced by:  ineq2 2214  ineq12 2215  ineq1i 2216  ineq1d 2219  unineq 2258  inex1g 2723  frc 2926  onnev 3248  reseq1 3374  isofrlem 3907  fiint 4572  fiintOLD 4573  inf3lema 4618  aceq5lem5 4749  kmlem12 4786  kmlem14 4788  inopnt 7601  isbasisg 7610  basis1t 7613  basis2t 7614  tgvalt 7615  subtop 7643  fctopOLD 7647  cctop 7649  elcls 7701  clsndisj 7703  elcls3 7708  islp2 7744  lpbl 7877  methausi 7878  omls 9241  pjomlt 9264  shinclt 9346  shmod 9358  chm0t 9409  chinclt 9417  chdmm1t 9443  ledit 9458  cmbrt 9522  cmbr3t 9546  mdbrt 10216  dmdmdt 10222  dmdit 10224  dmdbr3 10227  dmdbr4 10228  mdslmd1lem4 10250  cvmdt 10258  cvexcht 10296  dmdbr6at 10345  mddmdin0 10353  infi1 10441  intprd 10461  neiopne 10463  filint 10548  cnfilca 10562  dtt2 10589  ishgrag 10740  hgralem 10741  ispgrag 10750

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-in 2054

Copyright terms: Public domain