Metamath Proof Explorer

Theorem dfon2lem1

Description: Lemma for dfon2 . (Contributed by Scott Fenton, 28-Feb-2011)

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 nfsbc1v 
 |-  F/ x [. y / x ]. ph
3 nfv 
 |-  F/ x Tr y
4 nfsbc1v 
 |-  F/ x [. y / x ]. ps
5 2 3 4 nf3an 
 |-  F/ x ( [. y / x ]. ph /\ Tr y /\ [. y / x ]. ps )
6 vex 
 |-  y e. _V
7 sbceq1a 
 |-  ( x = y -> ( ph <-> [. y / x ]. ph ) )
8 treq 
 |-  ( x = y -> ( Tr x <-> Tr y ) )
9 sbceq1a 
 |-  ( x = y -> ( ps <-> [. y / x ]. ps ) )
10 7 8 9 3anbi123d 
 |-  ( x = y -> ( ( ph /\ Tr x /\ ps ) <-> ( [. y / x ]. ph /\ Tr y /\ [. y / x ]. ps ) ) )
11 5 6 10 elabf 
 |-  ( y e. { x | ( ph /\ Tr x /\ ps ) } <-> ( [. y / x ]. ph /\ Tr y /\ [. y / x ]. ps ) )
12 11 simp2bi 
 |-  ( y e. { x | ( ph /\ Tr x /\ ps ) } -> Tr y )
13 1 12 mprg 
 |-  Tr U. { x | ( ph /\ Tr x /\ ps ) }