| Step | Hyp | Ref | Expression | 
						
							| 1 |  | dfsclnbgr2.v |  |-  V = ( Vtx ` G ) | 
						
							| 2 |  | dfsclnbgr2.s |  |-  S = { n e. V | E. e e. E { N , n } C_ e } | 
						
							| 3 |  | dfsclnbgr2.e |  |-  E = ( Edg ` G ) | 
						
							| 4 | 2 | eleq2i |  |-  ( X e. S <-> X e. { n e. V | E. e e. E { N , n } C_ e } ) | 
						
							| 5 |  | preq2 |  |-  ( n = X -> { N , n } = { N , X } ) | 
						
							| 6 | 5 | sseq1d |  |-  ( n = X -> ( { N , n } C_ e <-> { N , X } C_ e ) ) | 
						
							| 7 | 6 | rexbidv |  |-  ( n = X -> ( E. e e. E { N , n } C_ e <-> E. e e. E { N , X } C_ e ) ) | 
						
							| 8 | 7 | elrab |  |-  ( X e. { n e. V | E. e e. E { N , n } C_ e } <-> ( X e. V /\ E. e e. E { N , X } C_ e ) ) | 
						
							| 9 | 4 8 | bitri |  |-  ( X e. S <-> ( X e. V /\ E. e e. E { N , X } C_ e ) ) |