Theorem ineq12 2264

Description: Equality theorem for intersection of two classes.

Assertion

Ref	Expression
ineq12	|- ((A = B /\ C = D) -> (A i^i C) = (B i^i D))

Proof of Theorem ineq12

Step	Hyp	Ref	Expression
1		ineq1 2262	. 2 |- (A = B -> (A i^i C) = (B i^i C))
2		ineq2 2263	. 2 |- (C = D -> (B i^i C) = (B i^i D))
3	1, 2	sylan9eq 1570	1 |- ((A = B /\ C = D) -> (A i^i C) = (B i^i D))

Syntax hints:   -> wi 3   /\ wa 221   = wceq 992   i^i cin 2098

This theorem is referenced by:  ineq12i 2267  ineqan12d 2271  ssin 2284  fnun 3700  endisj 4578  sbthlem8 4599  abfii4 4707  pm54.43 4715  kmlem9 4919  infxpidmlem11 7774  subbas 7856  subtop 7858  indistop 7860  retopbas 7865  ficli 10756  infi 10854  oefil2 11079  rcfpfillem4 11092  elfiun 11421  connsub 11502  filrn 11643  fmfnfmlem3 11702

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