Metamath Proof Explorer
		
		
		
		Description:  Unordered triple { A , B , A } is just an overlong way to write
     { A , B } .  (Contributed by David A. Wheeler, 10-May-2015)
		
			
				
					 | 
					 | 
					Ref | 
					Expression | 
				
				
					 | 
					Assertion | 
					tpidm13 | 
					   | 
				
			
		
		
			
				Proof
				
					
						| Step | 
						Hyp | 
						Ref | 
						Expression | 
					
						
							| 1 | 
							
								
							 | 
							tprot | 
							   | 
						
						
							| 2 | 
							
								
							 | 
							tpidm12 | 
							   | 
						
						
							| 3 | 
							
								1 2
							 | 
							eqtr3i | 
							   |