csbxpgVD

Description: Virtual deduction proof of csbxp . 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 is csbxpgVD without virtual deductions and was automatically derived from csbxpgVD .

		Ref	Expression
	Assertion	csbxpgVD	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		idn1	⊢ ( 𝐴 ∈ 𝑉 ▶ 𝐴 ∈ 𝑉 )
2		sbcel12	⊢ ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
3	2	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
4	1 3	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
5		csbconstg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑤 = 𝑤 )
6	1 5	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ 𝑤 = 𝑤 )
7		eleq1	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑤 = 𝑤 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
8	6 7	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
9		bibi1	⊢ ( ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
10	9	biimprd	⊢ ( ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
11	4 8 10	e11	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
12		sbcel12	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
13	12	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
14	1 13	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
15		csbconstg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 )
16	1 15	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 )
17		eleq1	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
18	16 17	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
19		bibi1	⊢ ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
20	19	biimprd	⊢ ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) → ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
21	14 18 20	e11	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
22		pm4.38	⊢ ( ( ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ∧ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) → ( ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
23	22	ex	⊢ ( ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) → ( ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
24	11 21 23	e11	⊢ ( 𝐴 ∈ 𝑉 ▶ ( ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
25		sbcan	⊢ ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) )
26	25	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ) )
27	1 26	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ) )
28		bibi1	⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ↔ ( ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
29	28	biimprcd	⊢ ( ( ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ) → ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
30	24 27 29	e11	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
31		sbcg	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ) )
32	1 31	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ) )
33		pm4.38	⊢ ( ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ) ∧ ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) → ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
34	33	expcom	⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) → ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ) → ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) ) )
35	30 32 34	e11	⊢ ( 𝐴 ∈ 𝑉 ▶ ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
36		sbcan	⊢ ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
37	36	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) )
38	1 37	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) )
39		bibi1	⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) ↔ ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) ) )
40	39	biimprcd	⊢ ( ( ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ [ 𝐴 / 𝑥 ] ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) → ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) ) )
41	35 38 40	e11	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
42	41	gen11	⊢ ( 𝐴 ∈ 𝑉 ▶ ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
43		exbi	⊢ ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) → ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
44	42 43	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
45		sbcex2	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
46	45	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) )
47	1 46	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) )
48		bibi1	⊢ ( ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) → ( ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) ↔ ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) ) )
49	48	biimprcd	⊢ ( ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) → ( ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) ) )
50	44 47 49	e11	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
51	50	gen11	⊢ ( 𝐴 ∈ 𝑉 ▶ ∀ 𝑤 ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
52		exbi	⊢ ( ∀ 𝑤 ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) → ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
53	51 52	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
54		sbcex2	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
55	54	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) )
56	1 55	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) )
57		bibi1	⊢ ( ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) → ( ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) ↔ ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) ) )
58	57	biimprcd	⊢ ( ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) → ( ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) → ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) ) )
59	53 56 58	e11	⊢ ( 𝐴 ∈ 𝑉 ▶ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
60	59	gen11	⊢ ( 𝐴 ∈ 𝑉 ▶ ∀ 𝑧 ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) )
61		abbi	⊢ ( ∀ 𝑧 ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) ↔ { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } )
62	61	biimpi	⊢ ( ∀ 𝑧 ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) ) → { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } )
63	60 62	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } )
64		csbab	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) }
65	64	a1i	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } )
66	1 65	e1a	⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } )
67		eqeq2	⊢ ( { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } ↔ ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } ) )
68	67	biimpd	⊢ ( { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } → ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } ) )
69	63 66 68	e11	⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } )
70		df-xp	⊢ ( 𝐵 × 𝐶 ) = { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) }
71		df-opab	⊢ { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) }
72	70 71	eqtri	⊢ ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) }
73	72	ax-gen	⊢ ∀ 𝑥 ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) }
74		csbeq2	⊢ ( ∀ 𝑥 ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } )
75	74	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } ) )
76	1 73 75	e10	⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } )
77		eqeq2	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } ) )
78	77	biimpd	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } ) )
79	69 76 78	e11	⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } )
80		df-xp	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) }
81		df-opab	⊢ { ⟨ 𝑤 , 𝑦 ⟩ ∣ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) } = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) }
82	80 81	eqtri	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) }
83		eqeq2	⊢ ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } ) )
84	83	biimprcd	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } → ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = { 𝑧 ∣ ∃ 𝑤 ∃ 𝑦 ( 𝑧 = ⟨ 𝑤 , 𝑦 ⟩ ∧ ( 𝑤 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
85	79 82 84	e10	⊢ ( 𝐴 ∈ 𝑉 ▶ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
86	85	in1	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 × ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )

1::	\|- (. A e. V ->. A e. V ).
2:1:	\|- (. A e. V ->. ( [. A / x ]. w e. B <-> [_ A / x ]_ w e. [_ A / x ]_ B ) ).
3:1:	\|- (. A e. V ->. [_ A / x ]_ w = w ).
4:3:	\|- (. A e. V ->. ( [_ A / x ]_ w e. [_ A / x ]_ B <-> w e. [_ A / x ]_ B ) ).
5:2,4:	\|- (. A e. V ->. ( [. A / x ]. w e. B <-> w e. [_ A / x ]_ B ) ).
6:1:	\|- (. A e. V ->. ( [. A / x ]. y e. C <-> [_ A / x ]_ y e. [_ A / x ]_ C ) ).
7:1:	\|- (. A e. V ->. [_ A / x ]_ y = y ).
8:7:	\|- (. A e. V ->. ( [_ A / x ]_ y e. [_ A / x ]_ C <-> y e. [_ A / x ]_ C ) ).
9:6,8:	\|- (. A e. V ->. ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ).
10:5,9:	\|- (. A e. V ->. ( ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ).
11:1:	\|- (. A e. V ->. ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) ) ).
12:10,11:	\|- (. A e. V ->. ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ).
13:1:	\|- (. A e. V ->. ( [. A / x ]. z = <. w ,. y >. <-> z = <. w , y >. ) ).
14:12,13:	\|- (. A e. V ->. ( ( [. A / x ]. z = <. w ,. y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
15:1:	\|- (. A e. V ->. ( [. A / x ]. ( z = <. w ,. y >. /\ ( w e. B /\ y e. C ) ) <-> ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) ) ).
16:14,15:	\|- (. A e. V ->. ( [. A / x ]. ( z = <. w ,. y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
17:16:	\|- (. A e. V ->. A. y ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
18:17:	\|- (. A e. V ->. ( E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
19:1:	\|- (. A e. V ->. ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ).
20:18,19:	\|- (. A e. V ->. ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
21:20:	\|- (. A e. V ->. A. w ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
22:21:	\|- (. A e. V ->. ( E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
23:1:	\|- (. A e. V ->. ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ).
24:22,23:	\|- (. A e. V ->. ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
25:24:	\|- (. A e. V ->. A. z ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
26:25:	\|- (. A e. V ->. { z \| [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z \| E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ).
27:1:	\|- (. A e. V ->. [_ A / x ]_ { z \| E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z \| [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ).
28:26,27:	\|- (. A e. V ->. [_ A / x ]_ { z \| E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z \| E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ).
29::	\|- { <. w ,. y >. \| ( w e. B /\ y e. C ) } = { z \| E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
30::	\|- ( B X. C ) = { <. w ,. y >. \| ( w e. B /\ y e. C ) }
31:29,30:	\|- ( B X. C ) = { z \| E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
32:31:	\|- A. x ( B X. C ) = { z \| E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
33:1,32:	\|- (. A e. V ->. [_ A / x ]_ ( B X. C ) = [_ A / x ]_ { z \| E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ).
34:28,33:	\|- (. A e. V ->. [_ A / x ]_ ( B X. C ) = { z \| E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ).
35::	\|- { <. w ,. y >. \| ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) } = { z \| E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) }
36::	\|- ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { <. w , y >. \| ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) }
37:35,36:	\|- ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { z \| E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) }
38:34,37:	\|- (. A e. V ->. [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) ).
qed:38:	\|- ( A e. V -> [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) )

Metamath Proof Explorer

Theorem csbxpgVD

Proof