Theorem brtp 5478

Description: A necessary and sufficient condition for two sets to be related under a binary relation which is 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 5086	. 2 ⊢ (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩})
2		opex 5416	. . 3 ⊢ ⟨𝑋, 𝑌⟩ ∈ V
3	2	eltp 4633	. 2 ⊢ (⟨𝑋, 𝑌⟩ ∈ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} ↔ (⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩))
4		brtp.1	. . . 4 ⊢ 𝑋 ∈ V
5		brtp.2	. . . 4 ⊢ 𝑌 ∈ V
6	4, 5	opth 5429	. . 3 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑋 = 𝐴 ∧ 𝑌 = 𝐵))
7	4, 5	opth 5429	. . 3 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷))
8	4, 5	opth 5429	. . 3 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹))
9	6, 7, 8	3orbi123i 1157	. 2 ⊢ ((⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩) ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹)))
10	1, 3, 9	3bitri 297	1 ⊢ (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹)))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  Vcvv 3429  {ctp 4571  ⟨cop 4573   class class class wbr 5085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-br 5086

This theorem is referenced by:  ltsval2  27620  ltsintdifex  27625  ltsres  27626  noextendlt  27633  noextendgt  27634  nolesgn2o  27635  nogesgn1o  27637  ltssolem1  27639  nosepnelem  27643  nosep1o  27645  nosep2o  27646  nosepdmlem  27647  nodenselem8  27655  nodense  27656  nolt02o  27659  nogt01o  27660  nosupbnd2lem1  27679  noinfbnd2lem1  27694