Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  br6 Structured version   Visualization version   GIF version

Theorem br6 30900
 Description: Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.)
Hypotheses
Ref Expression
br6.1 (𝑎 = 𝐴 → (𝜑𝜓))
br6.2 (𝑏 = 𝐵 → (𝜓𝜒))
br6.3 (𝑐 = 𝐶 → (𝜒𝜃))
br6.4 (𝑑 = 𝐷 → (𝜃𝜏))
br6.5 (𝑒 = 𝐸 → (𝜏𝜂))
br6.6 (𝑓 = 𝐹 → (𝜂𝜁))
br6.7 (𝑥 = 𝑋𝑃 = 𝑄)
br6.8 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)}
Assertion
Ref Expression
br6 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))
Distinct variable groups:   𝜒,𝑏   𝜂,𝑒   𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑝,𝑞,𝑃   𝑥,𝑝,𝜑,𝑞   𝜓,𝑎   𝑥,𝑎,𝐴,𝑏,𝑐,𝑑,𝑒,𝑓,𝑝,𝑞   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑝,𝑞,𝑥   𝑄,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑥   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑝,𝑞,𝑥   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑝,𝑞,𝑥   𝑋,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑥   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑝,𝑞,𝑥   𝜏,𝑑   𝜃,𝑐   𝜁,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑥   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑝,𝑞,𝑥   𝑆,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑝,𝑞,𝑥
Allowed substitution hints:   𝜑(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝜓(𝑥,𝑒,𝑓,𝑞,𝑝,𝑏,𝑐,𝑑)   𝜒(𝑥,𝑒,𝑓,𝑞,𝑝,𝑎,𝑐,𝑑)   𝜃(𝑥,𝑒,𝑓,𝑞,𝑝,𝑎,𝑏,𝑑)   𝜏(𝑥,𝑒,𝑓,𝑞,𝑝,𝑎,𝑏,𝑐)   𝜂(𝑥,𝑓,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑)   𝜁(𝑞,𝑝)   𝑃(𝑥)   𝑄(𝑞,𝑝)   𝑅(𝑥,𝑒,𝑓,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑)   𝑋(𝑞,𝑝)

Proof of Theorem br6
StepHypRef Expression
1 opex 4859 . . 3 𝐴, ⟨𝐵, 𝐶⟩⟩ ∈ V
2 opex 4859 . . 3 𝐷, ⟨𝐸, 𝐹⟩⟩ ∈ V
3 eqeq1 2614 . . . . . . . . 9 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩))
4 eqcom 2617 . . . . . . . . 9 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩)
53, 4syl6bb 275 . . . . . . . 8 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
653anbi1d 1395 . . . . . . 7 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → ((𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
76rexbidv 3034 . . . . . 6 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
872rexbidv 3039 . . . . 5 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
982rexbidv 3039 . . . 4 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
1092rexbidv 3039 . . 3 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
11 eqeq1 2614 . . . . . . . . 9 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩))
12 eqcom 2617 . . . . . . . . 9 (⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
1311, 12syl6bb 275 . . . . . . . 8 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
14133anbi2d 1396 . . . . . . 7 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
1514rexbidv 3034 . . . . . 6 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
16152rexbidv 3039 . . . . 5 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
17162rexbidv 3039 . . . 4 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
18172rexbidv 3039 . . 3 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
19 br6.8 . . 3 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)}
201, 2, 10, 18, 19brab 4923 . 2 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
21 vex 3176 . . . . . . . . . . . 12 𝑎 ∈ V
22 opex 4859 . . . . . . . . . . . 12 𝑏, 𝑐⟩ ∈ V
2321, 22opth 4871 . . . . . . . . . . 11 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ (𝑎 = 𝐴 ∧ ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩))
24 br6.1 . . . . . . . . . . . 12 (𝑎 = 𝐴 → (𝜑𝜓))
25 vex 3176 . . . . . . . . . . . . . 14 𝑏 ∈ V
26 vex 3176 . . . . . . . . . . . . . 14 𝑐 ∈ V
2725, 26opth 4871 . . . . . . . . . . . . 13 (⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩ ↔ (𝑏 = 𝐵𝑐 = 𝐶))
28 br6.2 . . . . . . . . . . . . . 14 (𝑏 = 𝐵 → (𝜓𝜒))
29 br6.3 . . . . . . . . . . . . . 14 (𝑐 = 𝐶 → (𝜒𝜃))
3028, 29sylan9bb 732 . . . . . . . . . . . . 13 ((𝑏 = 𝐵𝑐 = 𝐶) → (𝜓𝜃))
3127, 30sylbi 206 . . . . . . . . . . . 12 (⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩ → (𝜓𝜃))
3224, 31sylan9bb 732 . . . . . . . . . . 11 ((𝑎 = 𝐴 ∧ ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩) → (𝜑𝜃))
3323, 32sylbi 206 . . . . . . . . . 10 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝜑𝜃))
34 vex 3176 . . . . . . . . . . . 12 𝑑 ∈ V
35 opex 4859 . . . . . . . . . . . 12 𝑒, 𝑓⟩ ∈ V
3634, 35opth 4871 . . . . . . . . . . 11 (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ (𝑑 = 𝐷 ∧ ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩))
37 br6.4 . . . . . . . . . . . 12 (𝑑 = 𝐷 → (𝜃𝜏))
38 vex 3176 . . . . . . . . . . . . . 14 𝑒 ∈ V
39 vex 3176 . . . . . . . . . . . . . 14 𝑓 ∈ V
4038, 39opth 4871 . . . . . . . . . . . . 13 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑒 = 𝐸𝑓 = 𝐹))
41 br6.5 . . . . . . . . . . . . . 14 (𝑒 = 𝐸 → (𝜏𝜂))
42 br6.6 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 → (𝜂𝜁))
4341, 42sylan9bb 732 . . . . . . . . . . . . 13 ((𝑒 = 𝐸𝑓 = 𝐹) → (𝜏𝜁))
4440, 43sylbi 206 . . . . . . . . . . . 12 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ → (𝜏𝜁))
4537, 44sylan9bb 732 . . . . . . . . . . 11 ((𝑑 = 𝐷 ∧ ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩) → (𝜃𝜁))
4636, 45sylbi 206 . . . . . . . . . 10 (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝜃𝜁))
4733, 46sylan9bb 732 . . . . . . . . 9 ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩) → (𝜑𝜁))
4847biimp3a 1424 . . . . . . . 8 ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁)
4948a1i 11 . . . . . . 7 ((((((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) ∧ 𝑓𝑃) → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5049rexlimdva 3013 . . . . . 6 (((((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) → (∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5150rexlimdvva 3020 . . . . 5 ((((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5251rexlimdvva 3020 . . . 4 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5352rexlimdvva 3020 . . 3 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
54 simpl1 1057 . . . . 5 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → 𝑋𝑆)
55 simpl2 1058 . . . . . 6 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → (𝐴𝑄𝐵𝑄𝐶𝑄))
56 opeq1 4340 . . . . . . . . . 10 (𝑑 = 𝐷 → ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝑒, 𝑓⟩⟩)
5756eqeq1d 2612 . . . . . . . . 9 (𝑑 = 𝐷 → (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
5857, 373anbi23d 1394 . . . . . . . 8 (𝑑 = 𝐷 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜏)))
59 opeq1 4340 . . . . . . . . . . 11 (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
6059opeq2d 4347 . . . . . . . . . 10 (𝑒 = 𝐸 → ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝑓⟩⟩)
6160eqeq1d 2612 . . . . . . . . 9 (𝑒 = 𝐸 → (⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
6261, 413anbi23d 1394 . . . . . . . 8 (𝑒 = 𝐸 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜏) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂)))
63 opeq2 4341 . . . . . . . . . . . 12 (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
6463opeq2d 4347 . . . . . . . . . . 11 (𝑓 = 𝐹 → ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
6564eqeq1d 2612 . . . . . . . . . 10 (𝑓 = 𝐹 → (⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
6665, 423anbi23d 1394 . . . . . . . . 9 (𝑓 = 𝐹 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁)))
67 eqid 2610 . . . . . . . . . . 11 𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩
68 eqid 2610 . . . . . . . . . . 11 𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩
6967, 68pm3.2i 470 . . . . . . . . . 10 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
70 df-3an 1033 . . . . . . . . . 10 ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁) ↔ ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩) ∧ 𝜁))
7169, 70mpbiran 955 . . . . . . . . 9 ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁) ↔ 𝜁)
7266, 71syl6bb 275 . . . . . . . 8 (𝑓 = 𝐹 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂) ↔ 𝜁))
7358, 62, 72rspc3ev 3297 . . . . . . 7 (((𝐷𝑄𝐸𝑄𝐹𝑄) ∧ 𝜁) → ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃))
74733ad2antl3 1218 . . . . . 6 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃))
75 opeq1 4340 . . . . . . . . . . 11 (𝑎 = 𝐴 → ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝑏, 𝑐⟩⟩)
7675eqeq1d 2612 . . . . . . . . . 10 (𝑎 = 𝐴 → (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
7776, 243anbi13d 1393 . . . . . . . . 9 (𝑎 = 𝐴 → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
7877rexbidv 3034 . . . . . . . 8 (𝑎 = 𝐴 → (∃𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
79782rexbidv 3039 . . . . . . 7 (𝑎 = 𝐴 → (∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
80 opeq1 4340 . . . . . . . . . . . 12 (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
8180opeq2d 4347 . . . . . . . . . . 11 (𝑏 = 𝐵 → ⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝑐⟩⟩)
8281eqeq1d 2612 . . . . . . . . . 10 (𝑏 = 𝐵 → (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
8382, 283anbi13d 1393 . . . . . . . . 9 (𝑏 = 𝐵 → ((⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
8483rexbidv 3034 . . . . . . . 8 (𝑏 = 𝐵 → (∃𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ ∃𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
85842rexbidv 3039 . . . . . . 7 (𝑏 = 𝐵 → (∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
86 opeq2 4341 . . . . . . . . . . . 12 (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
8786opeq2d 4347 . . . . . . . . . . 11 (𝑐 = 𝐶 → ⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩)
8887eqeq1d 2612 . . . . . . . . . 10 (𝑐 = 𝐶 → (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
8988, 293anbi13d 1393 . . . . . . . . 9 (𝑐 = 𝐶 → ((⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
9089rexbidv 3034 . . . . . . . 8 (𝑐 = 𝐶 → (∃𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ ∃𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
91902rexbidv 3039 . . . . . . 7 (𝑐 = 𝐶 → (∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
9279, 85, 91rspc3ev 3297 . . . . . 6 (((𝐴𝑄𝐵𝑄𝐶𝑄) ∧ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)) → ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
9355, 74, 92syl2anc 691 . . . . 5 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
94 br6.7 . . . . . . 7 (𝑥 = 𝑋𝑃 = 𝑄)
9594rexeqdv 3122 . . . . . . . . . . 11 (𝑥 = 𝑋 → (∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9694, 95rexeqbidv 3130 . . . . . . . . . 10 (𝑥 = 𝑋 → (∃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9794, 96rexeqbidv 3130 . . . . . . . . 9 (𝑥 = 𝑋 → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9894, 97rexeqbidv 3130 . . . . . . . 8 (𝑥 = 𝑋 → (∃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9994, 98rexeqbidv 3130 . . . . . . 7 (𝑥 = 𝑋 → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
10094, 99rexeqbidv 3130 . . . . . 6 (𝑥 = 𝑋 → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
101100rspcev 3282 . . . . 5 ((𝑋𝑆 ∧ ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)) → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
10254, 93, 101syl2anc 691 . . . 4 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
103102ex 449 . . 3 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (𝜁 → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
10453, 103impbid 201 . 2 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ 𝜁))
10520, 104syl5bb 271 1 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∃wrex 2897  ⟨cop 4131   class class class wbr 4583  {copab 4642 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644 This theorem is referenced by:  brcgr3  31323
 Copyright terms: Public domain W3C validator