This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ⊆ ∩ { 𝑥 ∣ 𝜑 } → ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ 𝜑 ) } = ∩ { 𝑥 ∣ 𝜑 } )