This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ifpsnprss

Description: Lemma for wlkvtxeledg : Two adjacent (not necessarily different) vertices A and B in a walk are incident with an edge E . (Contributed by AV, 4-Apr-2021) (Revised by AV, 5-Nov-2021)

Ref Expression
Assertion ifpsnprss 
|- ( if- ( A = B , E = { A } , { A , B } C_ E ) -> { A , B } C_ E )

Proof

Step Hyp Ref Expression
1 ssidd 
 |-  ( ( A = B /\ E = { A } ) -> { A } C_ { A } )
2 preq2 
 |-  ( B = A -> { A , B } = { A , A } )
3 dfsn2 
 |-  { A } = { A , A }
4 2 3 eqtr4di 
 |-  ( B = A -> { A , B } = { A } )
5 4 eqcoms 
 |-  ( A = B -> { A , B } = { A } )
6 5 adantr 
 |-  ( ( A = B /\ E = { A } ) -> { A , B } = { A } )
7 simpr 
 |-  ( ( A = B /\ E = { A } ) -> E = { A } )
8 1 6 7 3sstr4d 
 |-  ( ( A = B /\ E = { A } ) -> { A , B } C_ E )
9 8 1fpid3 
 |-  ( if- ( A = B , E = { A } , { A , B } C_ E ) -> { A , B } C_ E )