Theorem iinrab2 4030

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 3984	. . . . . 6 ⊢ (A = ∅ → ∩x ∈ A {y ∈ B ∣ φ} = ∩x ∈ ∅ {y ∈ B ∣ φ})
2		0iin 4025	. . . . . 6 ⊢ ∩x ∈ ∅ {y ∈ B ∣ φ} = V
3	1, 2	syl6eq 2401	. . . . 5 ⊢ (A = ∅ → ∩x ∈ A {y ∈ B ∣ φ} = V)
4	3	ineq1d 3457	. . . 4 ⊢ (A = ∅ → (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = (V ∩ B))
5		incom 3449	. . . . 5 ⊢ (V ∩ B) = (B ∩ V)
6		inv1 3578	. . . . 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 3652	. . . 4 ⊢ (A = ∅ → ∀x ∈ A ∀y ∈ B φ)
10		rabid2 2789	. . . . 5 ⊢ (B = {y ∈ B ∣ ∀x ∈ A φ} ↔ ∀y ∈ B ∀x ∈ A φ)
11		ralcom 2772	. . . . 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 4029	. . . 4 ⊢ (A ≠ ∅ → ∩x ∈ A {y ∈ B ∣ φ} = {y ∈ B ∣ ∀x ∈ A φ})
16	15	ineq1d 3457	. . 3 ⊢ (A ≠ ∅ → (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = ({y ∈ B ∣ ∀x ∈ A φ} ∩ B))
17		ssrab2 3352	. . . 4 ⊢ {y ∈ B ∣ ∀x ∈ A φ} ⊆ B
18		dfss 3261	. . . 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 2593	1 ⊢ (∩x ∈ A {y ∈ B ∣ φ} ∩ B) = {y ∈ B ∣ ∀x ∈ A φ}

Syntax hints:   = wceq 1642   ≠ wne 2517  ∀wral 2615  {crab 2619  Vcvv 2860   ∩ cin 3209   ⊆ wss 3258  ∅c0 3551  ∩ciin 3971

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 2479  df-ne 2519  df-ral 2620  df-rab 2624  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-dif 3216  df-ss 3260  df-nul 3552  df-iin 3973

This theorem is referenced by: (None)