intabs

Description: Absorption of a redundant conjunct in the intersection of a class abstraction. (Contributed by NM, 3-Jul-2005)

	Ref	Expression
Hypotheses	intabs.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	intabs.2	⊢ ( 𝑥 = ∩ { 𝑦 ∣ 𝜓 } → ( 𝜑 ↔ 𝜒 ) )
	intabs.3	⊢ ( ∩ { 𝑦 ∣ 𝜓 } ⊆ 𝐴 ∧ 𝜒 )
Assertion	intabs	⊢ ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } = ∩ { 𝑥 ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		intabs.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		intabs.2	⊢ ( 𝑥 = ∩ { 𝑦 ∣ 𝜓 } → ( 𝜑 ↔ 𝜒 ) )
3		intabs.3	⊢ ( ∩ { 𝑦 ∣ 𝜓 } ⊆ 𝐴 ∧ 𝜒 )
4		sseq1	⊢ ( 𝑥 = ∩ { 𝑦 ∣ 𝜓 } → ( 𝑥 ⊆ 𝐴 ↔ ∩ { 𝑦 ∣ 𝜓 } ⊆ 𝐴 ) )
5	4 2	anbi12d	⊢ ( 𝑥 = ∩ { 𝑦 ∣ 𝜓 } → ( ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) ↔ ( ∩ { 𝑦 ∣ 𝜓 } ⊆ 𝐴 ∧ 𝜒 ) ) )
6	5 3	intmin3	⊢ ( ∩ { 𝑦 ∣ 𝜓 } ∈ V → ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ⊆ ∩ { 𝑦 ∣ 𝜓 } )
7		intnex	⊢ ( ¬ ∩ { 𝑦 ∣ 𝜓 } ∈ V ↔ ∩ { 𝑦 ∣ 𝜓 } = V )
8		ssv	⊢ ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ⊆ V
9		sseq2	⊢ ( ∩ { 𝑦 ∣ 𝜓 } = V → ( ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ⊆ ∩ { 𝑦 ∣ 𝜓 } ↔ ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ⊆ V ) )
10	8 9	mpbiri	⊢ ( ∩ { 𝑦 ∣ 𝜓 } = V → ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ⊆ ∩ { 𝑦 ∣ 𝜓 } )
11	7 10	sylbi	⊢ ( ¬ ∩ { 𝑦 ∣ 𝜓 } ∈ V → ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ⊆ ∩ { 𝑦 ∣ 𝜓 } )
12	6 11	pm2.61i	⊢ ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ⊆ ∩ { 𝑦 ∣ 𝜓 }
13	1	cbvabv	⊢ { 𝑥 ∣ 𝜑 } = { 𝑦 ∣ 𝜓 }
14	13	inteqi	⊢ ∩ { 𝑥 ∣ 𝜑 } = ∩ { 𝑦 ∣ 𝜓 }
15	12 14	sseqtrri	⊢ ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ⊆ ∩ { 𝑥 ∣ 𝜑 }
16		simpr	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) → 𝜑 )
17	16	ss2abi	⊢ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ⊆ { 𝑥 ∣ 𝜑 }
18		intss	⊢ ( { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } ⊆ { 𝑥 ∣ 𝜑 } → ∩ { 𝑥 ∣ 𝜑 } ⊆ ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } )
19	17 18	ax-mp	⊢ ∩ { 𝑥 ∣ 𝜑 } ⊆ ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) }
20	15 19	eqssi	⊢ ∩ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝜑 ) } = ∩ { 𝑥 ∣ 𝜑 }

Metamath Proof Explorer

Theorem intabs

Proof