Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  csbxpgVD Structured version   Visualization version   GIF version

Theorem csbxpgVD 41096
Description: Virtual deduction proof of csbxp 5648. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbxp 5648 is csbxpgVD 41096 without virtual deductions and was automatically derived from csbxpgVD 41096.
1:: (   𝐴𝑉   ▶   𝐴𝑉   )
2:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤𝐵 𝐴 / 𝑥𝑤𝐴 / 𝑥𝐵)   )
3:1: (   𝐴𝑉   ▶   𝐴 / 𝑥𝑤 = 𝑤   )
4:3: (   𝐴𝑉   ▶   (𝐴 / 𝑥𝑤𝐴 / 𝑥𝐵𝑤𝐴 / 𝑥𝐵)   )
5:2,4: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤𝐵𝑤 𝐴 / 𝑥𝐵)   )
6:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦𝐶 𝐴 / 𝑥𝑦𝐴 / 𝑥𝐶)   )
7:1: (   𝐴𝑉   ▶   𝐴 / 𝑥𝑦 = 𝑦   )
8:7: (   𝐴𝑉   ▶   (𝐴 / 𝑥𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐶)   )
9:6,8: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦𝐶𝑦 𝐴 / 𝑥𝐶)   )
10:5,9: (   𝐴𝑉   ▶   (([𝐴 / 𝑥]𝑤𝐵 [𝐴 / 𝑥]𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵 𝑦𝐴 / 𝑥𝐶))   )
11:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑤𝐵 𝑦𝐶) ↔ ([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶))   )
12:10,11: (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑤𝐵 𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))   )
13:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑧 = ⟨𝑤   ,    𝑦⟩ ↔ 𝑧 = ⟨𝑤, 𝑦⟩)   )
14:12,13: (   𝐴𝑉   ▶   (([𝐴 / 𝑥]𝑧 = ⟨𝑤    ,   𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦 ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
15:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑧 = ⟨𝑤    ,   𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦 [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)))   )
16:14,15: (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑧 = ⟨𝑤    ,   𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
17:16: (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥](𝑧 = 𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
18:17: (   𝐴𝑉   ▶   (∃𝑦[𝐴 / 𝑥](𝑧 = 𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
19:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦(𝑧 = 𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = 𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)))   )
20:18,19: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦(𝑧 = 𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
21:20: (   𝐴𝑉   ▶   𝑤([𝐴 / 𝑥]𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = 𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
22:21: (   𝐴𝑉   ▶   (∃𝑤[𝐴 / 𝑥]𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = 𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
23:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]𝑦 (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)))   )
24:22,23: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = 𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
25:24: (   𝐴𝑉   ▶   𝑧([𝐴 / 𝑥]𝑤 𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = 𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
26:25: (   𝐴𝑉   ▶   {𝑧[𝐴 / 𝑥]𝑤 𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}    )
27:1: (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑧 ∣ ∃𝑤 𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧[𝐴 / 𝑥] 𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}   )
28:26,27: (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑧 ∣ ∃𝑤 𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦( 𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}    )
29:: {⟨𝑤   ,   𝑦⟩ ∣ (𝑤𝐵𝑦𝐶)} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}
30:: (𝐵 × 𝐶) = {⟨𝑤   ,   𝑦⟩ ∣ (𝑤𝐵 𝑦𝐶)}
31:29,30: (𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤 , 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}
32:31: 𝑥(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = 𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}
33:1,32: (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 × 𝐶) = 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵 𝑦𝐶))}   )
34:28,33: (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵 𝑦𝐴 / 𝑥𝐶))}   )
35:: {⟨𝑤   ,   𝑦⟩ ∣ (𝑤𝐴 / 𝑥𝐵 𝑦𝐴 / 𝑥𝐶)} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}
36:: (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶) = { 𝑤, 𝑦⟩ ∣ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)}
37:35,36: (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵 𝑦𝐴 / 𝑥𝐶))}
38:34,37: (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 × 𝐶) = (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶)   )
qed:38: (𝐴𝑉𝐴 / 𝑥(𝐵 × 𝐶) = ( 𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶))
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbxpgVD (𝐴𝑉𝐴 / 𝑥(𝐵 × 𝐶) = (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶))

Proof of Theorem csbxpgVD
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 40776 . . . . . . . . . . . . . . . . . . 19 (   𝐴𝑉   ▶   𝐴𝑉   )
2 sbcel12 4363 . . . . . . . . . . . . . . . . . . . 20 ([𝐴 / 𝑥]𝑤𝐵𝐴 / 𝑥𝑤𝐴 / 𝑥𝐵)
32a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝐴𝑉 → ([𝐴 / 𝑥]𝑤𝐵𝐴 / 𝑥𝑤𝐴 / 𝑥𝐵))
41, 3e1a 40829 . . . . . . . . . . . . . . . . . 18 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤𝐵𝐴 / 𝑥𝑤𝐴 / 𝑥𝐵)   )
5 csbconstg 3905 . . . . . . . . . . . . . . . . . . . 20 (𝐴𝑉𝐴 / 𝑥𝑤 = 𝑤)
61, 5e1a 40829 . . . . . . . . . . . . . . . . . . 19 (   𝐴𝑉   ▶   𝐴 / 𝑥𝑤 = 𝑤   )
7 eleq1 2904 . . . . . . . . . . . . . . . . . . 19 (𝐴 / 𝑥𝑤 = 𝑤 → (𝐴 / 𝑥𝑤𝐴 / 𝑥𝐵𝑤𝐴 / 𝑥𝐵))
86, 7e1a 40829 . . . . . . . . . . . . . . . . . 18 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝑤𝐴 / 𝑥𝐵𝑤𝐴 / 𝑥𝐵)   )
9 bibi1 353 . . . . . . . . . . . . . . . . . . 19 (([𝐴 / 𝑥]𝑤𝐵𝐴 / 𝑥𝑤𝐴 / 𝑥𝐵) → (([𝐴 / 𝑥]𝑤𝐵𝑤𝐴 / 𝑥𝐵) ↔ (𝐴 / 𝑥𝑤𝐴 / 𝑥𝐵𝑤𝐴 / 𝑥𝐵)))
109biimprd 249 . . . . . . . . . . . . . . . . . 18 (([𝐴 / 𝑥]𝑤𝐵𝐴 / 𝑥𝑤𝐴 / 𝑥𝐵) → ((𝐴 / 𝑥𝑤𝐴 / 𝑥𝐵𝑤𝐴 / 𝑥𝐵) → ([𝐴 / 𝑥]𝑤𝐵𝑤𝐴 / 𝑥𝐵)))
114, 8, 10e11 40890 . . . . . . . . . . . . . . . . 17 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤𝐵𝑤𝐴 / 𝑥𝐵)   )
12 sbcel12 4363 . . . . . . . . . . . . . . . . . . . 20 ([𝐴 / 𝑥]𝑦𝐶𝐴 / 𝑥𝑦𝐴 / 𝑥𝐶)
1312a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦𝐶𝐴 / 𝑥𝑦𝐴 / 𝑥𝐶))
141, 13e1a 40829 . . . . . . . . . . . . . . . . . 18 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦𝐶𝐴 / 𝑥𝑦𝐴 / 𝑥𝐶)   )
15 csbconstg 3905 . . . . . . . . . . . . . . . . . . . 20 (𝐴𝑉𝐴 / 𝑥𝑦 = 𝑦)
161, 15e1a 40829 . . . . . . . . . . . . . . . . . . 19 (   𝐴𝑉   ▶   𝐴 / 𝑥𝑦 = 𝑦   )
17 eleq1 2904 . . . . . . . . . . . . . . . . . . 19 (𝐴 / 𝑥𝑦 = 𝑦 → (𝐴 / 𝑥𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐶))
1816, 17e1a 40829 . . . . . . . . . . . . . . . . . 18 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐶)   )
19 bibi1 353 . . . . . . . . . . . . . . . . . . 19 (([𝐴 / 𝑥]𝑦𝐶𝐴 / 𝑥𝑦𝐴 / 𝑥𝐶) → (([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶) ↔ (𝐴 / 𝑥𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐶)))
2019biimprd 249 . . . . . . . . . . . . . . . . . 18 (([𝐴 / 𝑥]𝑦𝐶𝐴 / 𝑥𝑦𝐴 / 𝑥𝐶) → ((𝐴 / 𝑥𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐶) → ([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶)))
2114, 18, 20e11 40890 . . . . . . . . . . . . . . . . 17 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶)   )
22 pm4.38 634 . . . . . . . . . . . . . . . . . 18 ((([𝐴 / 𝑥]𝑤𝐵𝑤𝐴 / 𝑥𝐵) ∧ ([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶)) → (([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))
2322ex 413 . . . . . . . . . . . . . . . . 17 (([𝐴 / 𝑥]𝑤𝐵𝑤𝐴 / 𝑥𝐵) → (([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶) → (([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))))
2411, 21, 23e11 40890 . . . . . . . . . . . . . . . 16 (   𝐴𝑉   ▶   (([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))   )
25 sbcan 3824 . . . . . . . . . . . . . . . . . 18 ([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ ([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶))
2625a1i 11 . . . . . . . . . . . . . . . . 17 (𝐴𝑉 → ([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ ([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶)))
271, 26e1a 40829 . . . . . . . . . . . . . . . 16 (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ ([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶))   )
28 bibi1 353 . . . . . . . . . . . . . . . . 17 (([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ ([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶)) → (([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)) ↔ (([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))))
2928biimprcd 251 . . . . . . . . . . . . . . . 16 ((([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)) → (([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ ([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶)) → ([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))))
3024, 27, 29e11 40890 . . . . . . . . . . . . . . 15 (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))   )
31 sbcg 3850 . . . . . . . . . . . . . . . 16 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ↔ 𝑧 = ⟨𝑤, 𝑦⟩))
321, 31e1a 40829 . . . . . . . . . . . . . . 15 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ↔ 𝑧 = ⟨𝑤, 𝑦⟩)   )
33 pm4.38 634 . . . . . . . . . . . . . . . 16 ((([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ↔ 𝑧 = ⟨𝑤, 𝑦⟩) ∧ ([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))) → (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))))
3433expcom 414 . . . . . . . . . . . . . . 15 (([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)) → (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ↔ 𝑧 = ⟨𝑤, 𝑦⟩) → (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))))
3530, 32, 34e11 40890 . . . . . . . . . . . . . 14 (   𝐴𝑉   ▶   (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
36 sbcan 3824 . . . . . . . . . . . . . . . 16 ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)))
3736a1i 11 . . . . . . . . . . . . . . 15 (𝐴𝑉 → ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶))))
381, 37e1a 40829 . . . . . . . . . . . . . 14 (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)))   )
39 bibi1 353 . . . . . . . . . . . . . . 15 (([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶))) → (([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))) ↔ (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))))
4039biimprcd 251 . . . . . . . . . . . . . 14 ((([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))) → (([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶))) → ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))))
4135, 38, 40e11 40890 . . . . . . . . . . . . 13 (   𝐴𝑉   ▶   ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
4241gen11 40818 . . . . . . . . . . . 12 (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
43 exbi 1840 . . . . . . . . . . . 12 (∀𝑦([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))) → (∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))))
4442, 43e1a 40829 . . . . . . . . . . 11 (   𝐴𝑉   ▶   (∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
45 sbcex2 3837 . . . . . . . . . . . . 13 ([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)))
4645a1i 11 . . . . . . . . . . . 12 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))))
471, 46e1a 40829 . . . . . . . . . . 11 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)))   )
48 bibi1 353 . . . . . . . . . . . 12 (([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))) → (([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))) ↔ (∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))))
4948biimprcd 251 . . . . . . . . . . 11 ((∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))) → (([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))) → ([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))))
5044, 47, 49e11 40890 . . . . . . . . . 10 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
5150gen11 40818 . . . . . . . . 9 (   𝐴𝑉   ▶   𝑤([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
52 exbi 1840 . . . . . . . . 9 (∀𝑤([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))) → (∃𝑤[𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))))
5351, 52e1a 40829 . . . . . . . 8 (   𝐴𝑉   ▶   (∃𝑤[𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
54 sbcex2 3837 . . . . . . . . . 10 ([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)))
5554a1i 11 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))))
561, 55e1a 40829 . . . . . . . 8 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)))   )
57 bibi1 353 . . . . . . . . 9 (([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))) → (([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))) ↔ (∃𝑤[𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))))
5857biimprcd 251 . . . . . . . 8 ((∃𝑤[𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))) → (([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))) → ([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))))
5953, 56, 58e11 40890 . . . . . . 7 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
6059gen11 40818 . . . . . 6 (   𝐴𝑉   ▶   𝑧([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))   )
61 abbi 2892 . . . . . . 7 (∀𝑧([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))) ↔ {𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))})
6261biimpi 217 . . . . . 6 (∀𝑧([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))) → {𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))})
6360, 62e1a 40829 . . . . 5 (   𝐴𝑉   ▶   {𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}   )
64 csbab 4392 . . . . . . 7 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}
6564a1i 11 . . . . . 6 (𝐴𝑉𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))})
661, 65e1a 40829 . . . . 5 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}   )
67 eqeq2 2837 . . . . . 6 ({𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))} → (𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} ↔ 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}))
6867biimpd 230 . . . . 5 ({𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))} → (𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} → 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}))
6963, 66, 68e11 40890 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}   )
70 df-xp 5559 . . . . . . 7 (𝐵 × 𝐶) = {⟨𝑤, 𝑦⟩ ∣ (𝑤𝐵𝑦𝐶)}
71 df-opab 5125 . . . . . . 7 {⟨𝑤, 𝑦⟩ ∣ (𝑤𝐵𝑦𝐶)} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}
7270, 71eqtri 2848 . . . . . 6 (𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}
7372ax-gen 1789 . . . . 5 𝑥(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}
74 csbeq2 3891 . . . . . 6 (∀𝑥(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} → 𝐴 / 𝑥(𝐵 × 𝐶) = 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))})
7574a1i 11 . . . . 5 (𝐴𝑉 → (∀𝑥(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} → 𝐴 / 𝑥(𝐵 × 𝐶) = 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}))
761, 73, 75e10 40896 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 × 𝐶) = 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}   )
77 eqeq2 2837 . . . . 5 (𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))} → (𝐴 / 𝑥(𝐵 × 𝐶) = 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} ↔ 𝐴 / 𝑥(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}))
7877biimpd 230 . . . 4 (𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))} → (𝐴 / 𝑥(𝐵 × 𝐶) = 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} → 𝐴 / 𝑥(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}))
7969, 76, 78e11 40890 . . 3 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}   )
80 df-xp 5559 . . . 4 (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶) = {⟨𝑤, 𝑦⟩ ∣ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)}
81 df-opab 5125 . . . 4 {⟨𝑤, 𝑦⟩ ∣ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}
8280, 81eqtri 2848 . . 3 (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}
83 eqeq2 2837 . . . 4 ((𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))} → (𝐴 / 𝑥(𝐵 × 𝐶) = (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶) ↔ 𝐴 / 𝑥(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}))
8483biimprcd 251 . . 3 (𝐴 / 𝑥(𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))} → ((𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))} → 𝐴 / 𝑥(𝐵 × 𝐶) = (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶)))
8579, 82, 84e10 40896 . 2 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 × 𝐶) = (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶)   )
8685in1 40773 1 (𝐴𝑉𝐴 / 𝑥(𝐵 × 𝐶) = (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1528   = wceq 1530  wex 1773  wcel 2107  {cab 2803  [wsbc 3775  csb 3886  cop 4569  {copab 5124   × cxp 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-nul 4295  df-opab 5125  df-xp 5559  df-vd1 40772
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator