Theorem brtp 31400

Description: A condition for a binary relation over an unordered triple. (Contributed by Scott Fenton, 8-Jun-2011.)

Hypotheses

Ref	Expression
brtp.1	⊢ 𝑋 ∈ V
brtp.2	⊢ 𝑌 ∈ V

Assertion

Ref	Expression
brtp	⊢ (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹)))

Proof of Theorem brtp

Step	Hyp	Ref	Expression
1		df-br 4624	. 2 ⊢ (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩})
2		opex 4903	. . 3 ⊢ ⟨𝑋, 𝑌⟩ ∈ V
3	2	eltp 4208	. 2 ⊢ (⟨𝑋, 𝑌⟩ ∈ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} ↔ (⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩))
4		brtp.1	. . . 4 ⊢ 𝑋 ∈ V
5		brtp.2	. . . 4 ⊢ 𝑌 ∈ V
6	4, 5	opth 4915	. . 3 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑋 = 𝐴 ∧ 𝑌 = 𝐵))
7	4, 5	opth 4915	. . 3 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷))
8	4, 5	opth 4915	. . 3 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹))
9	6, 7, 8	3orbi123i 1250	. 2 ⊢ ((⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩) ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹)))
10	1, 3, 9	3bitri 286	1 ⊢ (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹)))

Syntax hints:   ↔ wb 196   ∧ wa 384   ∨ w3o 1035   = wceq 1480   ∈ wcel 1987  Vcvv 3190  {ctp 4159  ⟨cop 4161   class class class wbr 4623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-br 4624

This theorem is referenced by:  sltval2  31563  sltsgn1  31568  sltsgn2  31569  sltintdifex  31570  sltres  31571  noextendlt  31579  noextendgt  31580  sltsolem1  31581  nodenselem8  31604  nodense  31605  nobndup  31616  nobnddown  31617  nosepnelem  31618  nosepdmlem  31620