Theorem intmin4

Description: Elimination of a conjunct in a class intersection. (Contributed by NM, 31-Jul-2006)

	Ref	Expression
Assertion	intmin4	⊢ ( 𝐴 ⊆ ∩ { 𝑥 ∣ 𝜑 } → ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) } = ∩ { 𝑥 ∣ 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		ssintab	⊢ ( 𝐴 ⊆ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝜑 → 𝐴 ⊆ 𝑥 ) )
2		simpr	⊢ ( ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) → 𝜑 )
3		ancr	⊢ ( ( 𝜑 → 𝐴 ⊆ 𝑥 ) → ( 𝜑 → ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) ) )
4	2 3	impbid2	⊢ ( ( 𝜑 → 𝐴 ⊆ 𝑥 ) → ( ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) ↔ 𝜑 ) )
5	4	imbi1d	⊢ ( ( 𝜑 → 𝐴 ⊆ 𝑥 ) → ( ( ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 ) ↔ ( 𝜑 → 𝑦 ∈ 𝑥 ) ) )
6	5	alimi	⊢ ( ∀ 𝑥 ( 𝜑 → 𝐴 ⊆ 𝑥 ) → ∀ 𝑥 ( ( ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 ) ↔ ( 𝜑 → 𝑦 ∈ 𝑥 ) ) )
7		albi	⊢ ( ∀ 𝑥 ( ( ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 ) ↔ ( 𝜑 → 𝑦 ∈ 𝑥 ) ) → ( ∀ 𝑥 ( ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑦 ∈ 𝑥 ) ) )
8	6 7	syl	⊢ ( ∀ 𝑥 ( 𝜑 → 𝐴 ⊆ 𝑥 ) → ( ∀ 𝑥 ( ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑦 ∈ 𝑥 ) ) )
9	1 8	sylbi	⊢ ( 𝐴 ⊆ ∩ { 𝑥 ∣ 𝜑 } → ( ∀ 𝑥 ( ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑦 ∈ 𝑥 ) ) )
10		vex	⊢ 𝑦 ∈ V
11	10	elintab	⊢ ( 𝑦 ∈ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) } ↔ ∀ 𝑥 ( ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 ) )
12	10	elintab	⊢ ( 𝑦 ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝜑 → 𝑦 ∈ 𝑥 ) )
13	9 11 12	3bitr4g	⊢ ( 𝐴 ⊆ ∩ { 𝑥 ∣ 𝜑 } → ( 𝑦 ∈ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) } ↔ 𝑦 ∈ ∩ { 𝑥 ∣ 𝜑 } ) )
14	13	eqrdv	⊢ ( 𝐴 ⊆ ∩ { 𝑥 ∣ 𝜑 } → ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) } = ∩ { 𝑥 ∣ 𝜑 } )