Theorem brtp 5497

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 5104	. 2 ⊢ (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ⟨𝑋, 𝑌⟩ ∈ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩})
2		opex 5432	. . 3 ⊢ ⟨𝑋, 𝑌⟩ ∈ V
3	2	eltp 4650	. 2 ⊢ (⟨𝑋, 𝑌⟩ ∈ {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩} ↔ (⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩))
4		brtp.1	. . . 4 ⊢ 𝑋 ∈ V
5		brtp.2	. . . 4 ⊢ 𝑌 ∈ V
6	4, 5	opth 5445	. . 3 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑋 = 𝐴 ∧ 𝑌 = 𝐵))
7	4, 5	opth 5445	. . 3 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷))
8	4, 5	opth 5445	. . 3 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹))
9	6, 7, 8	3orbi123i 1174	. 2 ⊢ ((⟨𝑋, 𝑌⟩ = ⟨𝐴, 𝐵⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝑋, 𝑌⟩ = ⟨𝐸, 𝐹⟩) ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹)))
10	1, 3, 9	3bitri 300	1 ⊢ (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  Vcvv 3451  {ctp 4588  ⟨cop 4590   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-br 5104

This theorem is used by:  ltsval2  28006  ltsintdifex  28011  ltsres  28012  noextendlt  28019  noextendgt  28020  nolesgn2o  28021  nogesgn1o  28023  ltssolem1  28025  nosepnelem  28029  nosep1o  28031  nosep2o  28032  nosepdmlem  28033  nodenselem8  28041  nodense  28042  nolt02o  28045  nogt01o  28046  nosupbnd2lem1  28065  noinfbnd2lem1  28080