ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-iin Structured version   GIF version

Definition df-iin 3651
Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3650. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3683. Theorem intiin 3702 provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998.)
Assertion
Ref Expression
df-iin x A B = {yx A y B}
Distinct variable groups:   x,y   y,A   y,B
Allowed substitution hints:   A(x)   B(x)

Detailed syntax breakdown of Definition df-iin
StepHypRef Expression
1 vx . . 3 setvar x
2 cA . . 3 class A
3 cB . . 3 class B
41, 2, 3ciin 3649 . 2 class x A B
5 vy . . . . . 6 setvar y
65cv 1241 . . . . 5 class y
76, 3wcel 1390 . . . 4 wff y B
87, 1, 2wral 2300 . . 3 wff x A y B
98, 5cab 2023 . 2 class {yx A y B}
104, 9wceq 1242 1 wff x A B = {yx A y B}
Colors of variables: wff set class
This definition is referenced by:  eliin  3653  iineq1  3662  iineq2  3665  nfiinxy  3675  nfiinya  3677  nfii1  3679  dfiin2g  3681  cbviin  3686  intiin  3702  0iin  3706  viin  3707  iinxsng  3721  iinxprg  3722  iinuniss  3728  bdciin  9334
  Copyright terms: Public domain W3C validator