Theorem inintabd

Description: Value of the intersection of class with the intersection of a nonempty class. (Contributed by RP, 13-Aug-2020)

	Ref	Expression
Hypothesis	inintabd.x	|- ( ph -> E. x ps )
Assertion	inintabd	|- ( ph -> ( A i^i |^| { x | ps } ) = |^| { w e. ~P A | E. x ( w = ( A i^i x ) /\ ps ) } )

Proof

Step	Hyp	Ref	Expression
1		inintabd.x	|- ( ph -> E. x ps )
2		pm5.5	|- ( E. x ps -> ( ( E. x ps -> u e. A ) <-> u e. A ) )
3	1 2	syl	|- ( ph -> ( ( E. x ps -> u e. A ) <-> u e. A ) )
4	3	bicomd	|- ( ph -> ( u e. A <-> ( E. x ps -> u e. A ) ) )
5	4	anbi1d	|- ( ph -> ( ( u e. A /\ A. x ( ps -> u e. x ) ) <-> ( ( E. x ps -> u e. A ) /\ A. x ( ps -> u e. x ) ) ) )
6		elinintab	|- ( u e. ( A i^i |^| { x | ps } ) <-> ( u e. A /\ A. x ( ps -> u e. x ) ) )
7		elinintrab	|- ( u e. _V -> ( u e. |^| { w e. ~P A | E. x ( w = ( A i^i x ) /\ ps ) } <-> ( ( E. x ps -> u e. A ) /\ A. x ( ps -> u e. x ) ) ) )
8	7	elv	|- ( u e. |^| { w e. ~P A | E. x ( w = ( A i^i x ) /\ ps ) } <-> ( ( E. x ps -> u e. A ) /\ A. x ( ps -> u e. x ) ) )
9	5 6 8	3bitr4g	|- ( ph -> ( u e. ( A i^i |^| { x | ps } ) <-> u e. |^| { w e. ~P A | E. x ( w = ( A i^i x ) /\ ps ) } ) )
10	9	eqrdv	|- ( ph -> ( A i^i |^| { x | ps } ) = |^| { w e. ~P A | E. x ( w = ( A i^i x ) /\ ps ) } )