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- ( 𝐴 = 𝐵 , 𝐸 = { 𝐴 } , { 𝐴 , 𝐵 } ⊆ 𝐸 ) → { 𝐴 , 𝐵 } ⊆ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		ssidd	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → { 𝐴 } ⊆ { 𝐴 } )
2		preq2	⊢ ( 𝐵 = 𝐴 → { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } )
3		dfsn2	⊢ { 𝐴 } = { 𝐴 , 𝐴 }
4	2 3	eqtr4di	⊢ ( 𝐵 = 𝐴 → { 𝐴 , 𝐵 } = { 𝐴 } )
5	4	eqcoms	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 } )
6	5	adantr	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → { 𝐴 , 𝐵 } = { 𝐴 } )
7		simpr	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → 𝐸 = { 𝐴 } )
8	1 6 7	3sstr4d	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐸 = { 𝐴 } ) → { 𝐴 , 𝐵 } ⊆ 𝐸 )
9	8	1fpid3	⊢ ( if- ( 𝐴 = 𝐵 , 𝐸 = { 𝐴 } , { 𝐴 , 𝐵 } ⊆ 𝐸 ) → { 𝐴 , 𝐵 } ⊆ 𝐸 )