| 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 | 1 2 3 | sclnbgrel |  |-  ( N e. S <-> ( N e. V /\ E. e e. E { N , N } C_ e ) ) | 
						
							| 5 |  | dfsn2 |  |-  { N } = { N , N } | 
						
							| 6 | 5 | eqcomi |  |-  { N , N } = { N } | 
						
							| 7 | 6 | sseq1i |  |-  ( { N , N } C_ e <-> { N } C_ e ) | 
						
							| 8 |  | snssg |  |-  ( N e. V -> ( N e. e <-> { N } C_ e ) ) | 
						
							| 9 | 7 8 | bitr4id |  |-  ( N e. V -> ( { N , N } C_ e <-> N e. e ) ) | 
						
							| 10 | 9 | rexbidv |  |-  ( N e. V -> ( E. e e. E { N , N } C_ e <-> E. e e. E N e. e ) ) | 
						
							| 11 | 10 | pm5.32i |  |-  ( ( N e. V /\ E. e e. E { N , N } C_ e ) <-> ( N e. V /\ E. e e. E N e. e ) ) | 
						
							| 12 | 4 11 | bitri |  |-  ( N e. S <-> ( N e. V /\ E. e e. E N e. e ) ) |