Theorem iinrab2 4029

Description: Indexed intersection of a restricted class builder. (Contributed by NM, 6-Dec-2011.)

Assertion

Ref	Expression
iinrab2	⊢ (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = {y ∈ B ∣ ∀x ∈ A φ}

Distinct variable groups:   y,A,x   x,B,y

Allowed substitution hints:   φ(x,y)

Proof of Theorem iinrab2

Step	Hyp	Ref	Expression
1		iineq1 3983	. . . . . 6 ⊢ (A = ∅ → ∩x ∈ A {y ∈ B ∣ φ} = ∩x ∈ ∅ {y ∈ B ∣ φ})
2		0iin 4024	. . . . . 6 ⊢ ∩x ∈ ∅ {y ∈ B ∣ φ} = V
3	1, 2	syl6eq 2401	. . . . 5 ⊢ (A = ∅ → ∩x ∈ A {y ∈ B ∣ φ} = V)
4	3	ineq1d 3456	. . . 4 ⊢ (A = ∅ → (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = (V ∩ B))
5		incom 3448	. . . . 5 ⊢ (V ∩ B) = (B ∩ V)
6		inv1 3577	. . . . 5 ⊢ (B ∩ V) = B
7	5, 6	eqtri 2373	. . . 4 ⊢ (V ∩ B) = B
8	4, 7	syl6eq 2401	. . 3 ⊢ (A = ∅ → (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = B)
9		rzal 3651	. . . 4 ⊢ (A = ∅ → ∀x ∈ A ∀y ∈ B φ)
10		rabid2 2788	. . . . 5 ⊢ (B = {y ∈ B ∣ ∀x ∈ A φ} ↔ ∀y ∈ B ∀x ∈ A φ)
11		ralcom 2771	. . . . 5 ⊢ (∀y ∈ B ∀x ∈ A φ ↔ ∀x ∈ A ∀y ∈ B φ)
12	10, 11	bitr2i 241	. . . 4 ⊢ (∀x ∈ A ∀y ∈ B φ ↔ B = {y ∈ B ∣ ∀x ∈ A φ})
13	9, 12	sylib 188	. . 3 ⊢ (A = ∅ → B = {y ∈ B ∣ ∀x ∈ A φ})
14	8, 13	eqtrd 2385	. 2 ⊢ (A = ∅ → (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = {y ∈ B ∣ ∀x ∈ A φ})
15		iinrab 4028	. . . 4 ⊢ (A ≠ ∅ → ∩x ∈ A {y ∈ B ∣ φ} = {y ∈ B ∣ ∀x ∈ A φ})
16	15	ineq1d 3456	. . 3 ⊢ (A ≠ ∅ → (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = ({y ∈ B ∣ ∀x ∈ A φ} ∩ B))
17		ssrab2 3351	. . . 4 ⊢ {y ∈ B ∣ ∀x ∈ A φ} ⊆ B
18		dfss 3260	. . . 4 ⊢ ({y ∈ B ∣ ∀x ∈ A φ} ⊆ B ↔ {y ∈ B ∣ ∀x ∈ A φ} = ({y ∈ B ∣ ∀x ∈ A φ} ∩ B))
19	17, 18	mpbi 199	. . 3 ⊢ {y ∈ B ∣ ∀x ∈ A φ} = ({y ∈ B ∣ ∀x ∈ A φ} ∩ B)
20	16, 19	syl6eqr 2403	. 2 ⊢ (A ≠ ∅ → (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = {y ∈ B ∣ ∀x ∈ A φ})
21	14, 20	pm2.61ine 2592	1 ⊢ (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = {y ∈ B ∣ ∀x ∈ A φ}

Syntax hints:   = wceq 1642   ≠ wne 2516  ∀wral 2614  {crab 2618  Vcvv 2859   ∩ cin 3208   ⊆ wss 3257  ∅c0 3550  ∩ciin 3970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rab 2623  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-dif 3215  df-ss 3259  df-nul 3551  df-iin 3972

This theorem is referenced by: (None)