Theorem rintn0

Description: Relative intersection of a nonempty set. (Contributed by Stefan O'Rear, 3-Apr-2015) (Revised by Mario Carneiro, 5-Jun-2015)

	Ref	Expression
Assertion	rintn0	|- ( ( X C_ ~P A /\ X =/= (/) ) -> ( A i^i |^| X ) = |^| X )

Proof

Step	Hyp	Ref	Expression
1		intssuni2	|- ( ( X C_ ~P A /\ X =/= (/) ) -> |^| X C_ U. ~P A )
2		ssid	|- ~P A C_ ~P A
3		sspwuni	|- ( ~P A C_ ~P A <-> U. ~P A C_ A )
4	2 3	mpbi	|- U. ~P A C_ A
5	1 4	sstrdi	|- ( ( X C_ ~P A /\ X =/= (/) ) -> |^| X C_ A )
6		sseqin2	|- ( |^| X C_ A <-> ( A i^i |^| X ) = |^| X )
7	5 6	sylib	|- ( ( X C_ ~P A /\ X =/= (/) ) -> ( A i^i |^| X ) = |^| X )