Theorem brtpid1

Description: A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016)

	Ref	Expression
Assertion	brtpid1	⊢ 𝐴 { ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 , 𝐷 } 𝐵

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
2	1	tpid1	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 , 𝐷 }
3		df-br	⊢ ( 𝐴 { ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 , 𝐷 } 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 , 𝐷 } )
4	2 3	mpbir	⊢ 𝐴 { ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 , 𝐷 } 𝐵