Theorem brtpid3

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

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

Proof

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