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

Metamath Proof Explorer

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 ) )