Theorem ss2abdv

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011) Avoid ax-8 , ax-10 , ax-11 , ax-12 . (Revised by Gino Giotto, 28-Jun-2024)

	Ref	Expression
Hypothesis	ss2abdv.1	|- ( ph -> ( ps -> ch ) )
Assertion	ss2abdv	|- ( ph -> { x | ps } C_ { x | ch } )

Proof

Step	Hyp	Ref	Expression
1		ss2abdv.1	|- ( ph -> ( ps -> ch ) )
2		df-in	|- ( { x | ps } i^i { x | ch } ) = { y | ( y e. { x | ps } /\ y e. { x | ch } ) }
3		df-clab	|- ( y e. { x | ps } <-> [ y / x ] ps )
4	3	bicomi	|- ( [ y / x ] ps <-> y e. { x | ps } )
5		df-clab	|- ( y e. { x | ch } <-> [ y / x ] ch )
6	5	bicomi	|- ( [ y / x ] ch <-> y e. { x | ch } )
7	4 6	anbi12i	|- ( ( [ y / x ] ps /\ [ y / x ] ch ) <-> ( y e. { x | ps } /\ y e. { x | ch } ) )
8	7	abbii	|- { y | ( [ y / x ] ps /\ [ y / x ] ch ) } = { y | ( y e. { x | ps } /\ y e. { x | ch } ) }
9		sbequ	|- ( y = z -> ( [ y / x ] ps <-> [ z / x ] ps ) )
10		sbequ	|- ( y = z -> ( [ y / x ] ch <-> [ z / x ] ch ) )
11	9 10	anbi12d	|- ( y = z -> ( ( [ y / x ] ps /\ [ y / x ] ch ) <-> ( [ z / x ] ps /\ [ z / x ] ch ) ) )
12	11	sbievw	|- ( [ z / y ] ( [ y / x ] ps /\ [ y / x ] ch ) <-> ( [ z / x ] ps /\ [ z / x ] ch ) )
13		ax-1	|- ( [ z / x ] ps -> ( [ z / x ] ch -> [ z / x ] ps ) )
14	13	a1i	|- ( ph -> ( [ z / x ] ps -> ( [ z / x ] ch -> [ z / x ] ps ) ) )
15	14	impd	|- ( ph -> ( ( [ z / x ] ps /\ [ z / x ] ch ) -> [ z / x ] ps ) )
16	1	sbimdv	|- ( ph -> ( [ z / x ] ps -> [ z / x ] ch ) )
17	16	ancld	|- ( ph -> ( [ z / x ] ps -> ( [ z / x ] ps /\ [ z / x ] ch ) ) )
18	15 17	impbid	|- ( ph -> ( ( [ z / x ] ps /\ [ z / x ] ch ) <-> [ z / x ] ps ) )
19	12 18	syl5bb	|- ( ph -> ( [ z / y ] ( [ y / x ] ps /\ [ y / x ] ch ) <-> [ z / x ] ps ) )
20		df-clab	|- ( z e. { y | ( [ y / x ] ps /\ [ y / x ] ch ) } <-> [ z / y ] ( [ y / x ] ps /\ [ y / x ] ch ) )
21		df-clab	|- ( z e. { x | ps } <-> [ z / x ] ps )
22	19 20 21	3bitr4g	|- ( ph -> ( z e. { y | ( [ y / x ] ps /\ [ y / x ] ch ) } <-> z e. { x | ps } ) )
23	22	eqrdv	|- ( ph -> { y | ( [ y / x ] ps /\ [ y / x ] ch ) } = { x | ps } )
24	8 23	syl5eqr	|- ( ph -> { y | ( y e. { x | ps } /\ y e. { x | ch } ) } = { x | ps } )
25	2 24	syl5eq	|- ( ph -> ( { x | ps } i^i { x | ch } ) = { x | ps } )
26		df-ss	|- ( { x | ps } C_ { x | ch } <-> ( { x | ps } i^i { x | ch } ) = { x | ps } )
27	25 26	sylibr	|- ( ph -> { x | ps } C_ { x | ch } )