Theorem dfon2lem1

Description: Lemma for dfon2 . (Contributed by Scott Fenton, 28-Feb-2011) (Proof shortened by SN, 5-Oct-2026)

	Ref	Expression
Assertion	dfon2lem1	|- Tr U. { x | ( ph /\ Tr x /\ ps ) }

Proof

Step	Hyp	Ref	Expression
1		truni	|- ( A. y e. { x | ( ph /\ Tr x /\ ps ) } Tr y -> Tr U. { x | ( ph /\ Tr x /\ ps ) } )
2		simp2	|- ( ( ph /\ Tr x /\ ps ) -> Tr x )
3	2	ss2abi	|- { x | ( ph /\ Tr x /\ ps ) } C_ { x | Tr x }
4	3	sseli	|- ( y e. { x | ( ph /\ Tr x /\ ps ) } -> y e. { x | Tr x } )
5		vex	|- y e. _V
6		treq	|- ( x = y -> ( Tr x <-> Tr y ) )
7	5 6	elab	|- ( y e. { x | Tr x } <-> Tr y )
8	4 7	sylib	|- ( y e. { x | ( ph /\ Tr x /\ ps ) } -> Tr y )
9	1 8	mprg	|- Tr U. { x | ( ph /\ Tr x /\ ps ) }