Theorem csbxpgVD 41221

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

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.

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1531   = wceq 1533  ∃wex 1776   ∈ wcel 2110  {cab 2799  [wsbc 3771  ⦋csb 3882  ⟨cop 4566  {copab 5120   × cxp 5547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-nul 4291  df-opab 5121  df-xp 5555  df-vd1 40897

This theorem is referenced by: (None)