Theorem ifpprsnss

Description: An unordered pair is a singleton or a subset of itself. This theorem is helpful to convert theorems about walks in arbitrary graphs into theorems about walks in pseudographs. (Contributed by AV, 27-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		preq2	|- ( B = A -> { A , B } = { A , A } )
2		dfsn2	|- { A } = { A , A }
3	1 2	eqtr4di	|- ( B = A -> { A , B } = { A } )
4	3	eqcoms	|- ( A = B -> { A , B } = { A } )
5	4	eqeq2d	|- ( A = B -> ( P = { A , B } <-> P = { A } ) )
6	5	biimpac	|- ( ( P = { A , B } /\ A = B ) -> P = { A } )
7		eqimss2	|- ( P = { A , B } -> { A , B } C_ P )
8	7	adantr	|- ( ( P = { A , B } /\ -. A = B ) -> { A , B } C_ P )
9	6 8	ifpimpda	|- ( P = { A , B } -> if- ( A = B , P = { A } , { A , B } C_ P ) )