Theorem csbingVD 45620

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

1::	⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2::	⊢ (𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) }
20:2:	⊢ ∀𝑥(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}
30:1,20:	⊢ (   𝐴 ∈ 𝐵   ▶   [𝐴 / 𝑥](𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
3:1,30:	⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
4:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
5:3,4:	⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
6:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)   )
7:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)   )
8:6,7:	⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷 ))   )
9:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷))   )
10:9,8:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
11:10:	⊢ (   𝐴 ∈ 𝐵   ▶   ∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
12:11:	⊢ (   𝐴 ∈ 𝐵   ▶   {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}   )
13:5,12:	⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}   )
14::	⊢ (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷) = { 𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}
15:13,14:	⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷)   )
qed:15:	⊢ (𝐴 ∈ 𝐵 → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ( ⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷))

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
csbingVD	⊢ (𝐴 ∈ 𝐵 → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷))

Proof of Theorem csbingVD

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn1 45311	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2		df-in 3911	. . . . . . . 8 ⊢ (𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}
3	2	ax-gen 1824	. . . . . . 7 ⊢ ∀𝑥(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}
4		spsbc 3756	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → [𝐴 / 𝑥](𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}))
5	1, 3, 4	e10 45431	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   [𝐴 / 𝑥](𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
6		sbceqg 4376	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} ↔ ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}))
7	6	biimpd 232	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}))
8	1, 5, 7	e11 45425	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
9		csbab 4404	. . . . . . 7 ⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}
10	9	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)})
11	1, 10	e1a 45364	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
12		eqeq1 2766	. . . . . 6 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} ↔ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}))
13	12	biimprd 251	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → (⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}))
14	8, 11, 13	e11 45425	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
15		sbcan 3792	. . . . . . . . 9 ⊢ ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷))
16	15	a1i 11	. . . . . . . 8 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷)))
17	1, 16	e1a 45364	. . . . . . 7 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷))   )
18		sbcel2 4382	. . . . . . . . . 10 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)
19	18	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))
20	1, 19	e1a 45364	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)   )
21		sbcel2 4382	. . . . . . . . . 10 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)
22	21	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))
23	1, 22	e1a 45364	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)   )
24		pm4.38 648	. . . . . . . . 9 ⊢ ((([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶) ∧ ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)))
25	24	ex 417	. . . . . . . 8 ⊢ (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶) → (([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷) → (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
26	20, 23, 25	e11 45425	. . . . . . 7 ⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
27		bibi1 354	. . . . . . . 8 ⊢ (([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷)) → (([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ↔ (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
28	27	biimprd 251	. . . . . . 7 ⊢ (([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷)) → ((([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
29	17, 26, 28	e11 45425	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
30	29	gen11 45353	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
31		abbib 2831	. . . . . 6 ⊢ ({𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)} ↔ ∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)))
32	31	biimpri 231	. . . . 5 ⊢ (∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)})
33	30, 32	e1a 45364	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}   )
34		eqeq1 2766	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)} ↔ {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}))
35	34	biimprd 251	. . . 4 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → ({𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)} → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}))
36	14, 33, 35	e11 45425	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}   )
37		df-in 3911	. . 3 ⊢ (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}
38		eqeq2 2774	. . . 4 ⊢ ((⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)} → (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷) ↔ ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}))
39	38	biimprcd 253	. . 3 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)} → ((⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)} → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷)))
40	36, 37, 39	e10 45431	. 2 ⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷)   )
41	40	in1 45308	1 ⊢ (𝐴 ∈ 𝐵 → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1567   = wceq 1569   ∈ wcel 2142  {cab 2740  [wsbc 3743  ⦋csb 3852   ∩ cin 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-in 3911  df-nul 4286  df-vd1 45307

This theorem is used by: (None)