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 )