Theorem brtpid2

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

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

Proof

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