Theorem intabs 2729

Description: Absorption of a redundant conjunct in the intersection of a class abstraction.

Hypotheses

Ref	Expression
intabs.1	⊢ (x = y → (φ ↔ ψ))
intabs.2	⊢ (x = ∩{y∣ψ} → (φ ↔ χ))
intabs.3	⊢ (∩{y∣ψ} ⊆ A ⋀ χ)

Assertion

Ref	Expression
intabs	⊢ ∩{x∣(x ⊆ A ⋀ φ)} = ∩{x∣φ}

Distinct variable groups:   x,y   x,A   φ,y   ψ,x   χ,x

Proof of Theorem intabs

Step	Hyp	Ref	Expression
1		sseq1 2078	. . . . . 6 ⊢ (x = ∩{y∣ψ} → (x ⊆ A ↔ ∩{y∣ψ} ⊆ A))
2		intabs.2	. . . . . 6 ⊢ (x = ∩{y∣ψ} → (φ ↔ χ))
3	1, 2	anbi12d 627	. . . . 5 ⊢ (x = ∩{y∣ψ} → ((x ⊆ A ⋀ φ) ↔ (∩{y∣ψ} ⊆ A ⋀ χ)))
4		intabs.3	. . . . 5 ⊢ (∩{y∣ψ} ⊆ A ⋀ χ)
5	3, 4	intmin3 2554	. . . 4 ⊢ (∩{y∣ψ} ∈ V → ∩{x∣(x ⊆ A ⋀ φ)} ⊆ ∩{y∣ψ})
6		intnex 2726	. . . . 5 ⊢ (¬ ∩{y∣ψ} ∈ V ↔ ∩{y∣ψ} = V)
7		ssv 2077	. . . . . 6 ⊢ ∩{x∣(x ⊆ A ⋀ φ)} ⊆ V
8		sseq2 2079	. . . . . 6 ⊢ (∩{y∣ψ} = V → (∩{x∣(x ⊆ A ⋀ φ)} ⊆ ∩{y∣ψ} ↔ ∩{x∣(x ⊆ A ⋀ φ)} ⊆ V))
9	7, 8	mpbiri 194	. . . . 5 ⊢ (∩{y∣ψ} = V → ∩{x∣(x ⊆ A ⋀ φ)} ⊆ ∩{y∣ψ})
10	6, 9	sylbi 199	. . . 4 ⊢ (¬ ∩{y∣ψ} ∈ V → ∩{x∣(x ⊆ A ⋀ φ)} ⊆ ∩{y∣ψ})
11	5, 10	pm2.61i 126	. . 3 ⊢ ∩{x∣(x ⊆ A ⋀ φ)} ⊆ ∩{y∣ψ}
12		intabs.1	. . . . 5 ⊢ (x = y → (φ ↔ ψ))
13	12	cbvabv 1905	. . . 4 ⊢ {x∣φ} = {y∣ψ}
14	13	inteqi 2533	. . 3 ⊢ ∩{x∣φ} = ∩{y∣ψ}
15	11, 14	sseqtr4 2090	. 2 ⊢ ∩{x∣(x ⊆ A ⋀ φ)} ⊆ ∩{x∣φ}
16		pm3.27 323	. . . 4 ⊢ ((x ⊆ A ⋀ φ) → φ)
17	16	ss2abi 2116	. . 3 ⊢ {x∣(x ⊆ A ⋀ φ)} ⊆ {x∣φ}
18		intss 2550	. . 3 ⊢ ({x∣(x ⊆ A ⋀ φ)} ⊆ {x∣φ} → ∩{x∣φ} ⊆ ∩{x∣(x ⊆ A ⋀ φ)})
19	17, 18	ax-mp 7	. 2 ⊢ ∩{x∣φ} ⊆ ∩{x∣(x ⊆ A ⋀ φ)}
20	15, 19	eqssi 2074	1 ⊢ ∩{x∣(x ⊆ A ⋀ φ)} = ∩{x∣φ}

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223   = wceq 954   ∈ wcel 956  {cab 1461  Vcvv 1807   ⊆ wss 2043  ∩cint 2529

This theorem is referenced by:  dfnn2 5904

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2699

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-v 1808  df-dif 2045  df-in 2047  df-ss 2049  df-nul 2277  df-int 2530

Copyright terms: Public domain