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-\left(A=B,E=\left\{A\right\},\left\{A,B\right\}\subseteq E\right)\to \left\{A,B\right\}\subseteq E$$

Proof

Step	Hyp	Ref	Expression
1		ssidd	$$⊢\left(A=B\wedge E=\left\{A\right\}\right)\to \left\{A\right\}\subseteq \left\{A\right\}$$
2		preq2	$$⊢B=A\to \left\{A,B\right\}=\left\{A,A\right\}$$
3		dfsn2	$$⊢\left\{A\right\}=\left\{A,A\right\}$$
4	2 3	eqtr4di	$$⊢B=A\to \left\{A,B\right\}=\left\{A\right\}$$
5	4	eqcoms	$$⊢A=B\to \left\{A,B\right\}=\left\{A\right\}$$
6	5	adantr	$$⊢\left(A=B\wedge E=\left\{A\right\}\right)\to \left\{A,B\right\}=\left\{A\right\}$$
7		simpr	$$⊢\left(A=B\wedge E=\left\{A\right\}\right)\to E=\left\{A\right\}$$
8	1 6 7	3sstr4d	$$⊢\left(A=B\wedge E=\left\{A\right\}\right)\to \left\{A,B\right\}\subseteq E$$
9	8	1fpid3	$$⊢if-\left(A=B,E=\left\{A\right\},\left\{A,B\right\}\subseteq E\right)\to \left\{A,B\right\}\subseteq E$$