Theorem csbingVD 40782

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

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 40472	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2		df-in 3870	. . . . . . . 8 ⊢ (𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}
3	2	ax-gen 1777	. . . . . . 7 ⊢ ∀𝑥(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}
4		spsbc 3722	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → [𝐴 / 𝑥](𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}))
5	1, 3, 4	e10 40592	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   [𝐴 / 𝑥](𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
6		sbceqg 4285	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} ↔ ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}))
7	6	biimpd 230	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}))
8	1, 5, 7	e11 40586	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
9		csbab 4308	. . . . . . 7 ⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}
10	9	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)})
11	1, 10	e1a 40525	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
12		eqeq1 2799	. . . . . 6 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} ↔ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}))
13	12	biimprd 249	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → (⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}))
14	8, 11, 13	e11 40586	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)}   )
15		sbcan 3753	. . . . . . . . 9 ⊢ ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷))
16	15	a1i 11	. . . . . . . 8 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷)))
17	1, 16	e1a 40525	. . . . . . 7 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷))   )
18		sbcel2 4291	. . . . . . . . . 10 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)
19	18	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))
20	1, 19	e1a 40525	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)   )
21		sbcel2 4291	. . . . . . . . . 10 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)
22	21	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))
23	1, 22	e1a 40525	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)   )
24		pm4.38 634	. . . . . . . . 9 ⊢ ((([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶) ∧ ([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)))
25	24	ex 413	. . . . . . . 8 ⊢ (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶) → (([𝐴 / 𝑥]𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷) → (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
26	20, 23, 25	e11 40586	. . . . . . 7 ⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
27		bibi1 353	. . . . . . . 8 ⊢ (([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷)) → (([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ↔ (([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
28	27	biimprd 249	. . . . . . 7 ⊢ (([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷)) → ((([𝐴 / 𝑥]𝑦 ∈ 𝐶 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))))
29	17, 26, 28	e11 40586	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
30	29	gen11 40514	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷))   )
31		abbi 2924	. . . . . 6 ⊢ (∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) ↔ {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)})
32	31	biimpi 217	. . . . 5 ⊢ (∀𝑦([𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ↔ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)) → {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)})
33	30, 32	e1a 40525	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}   )
34		eqeq1 2799	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)} ↔ {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}))
35	34	biimprd 249	. . . 4 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} → ({𝑦 ∣ [𝐴 / 𝑥](𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)} = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)} → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}))
36	14, 33, 35	e11 40586	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}   )
37		df-in 3870	. . 3 ⊢ (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}
38		eqeq2 2806	. . . 4 ⊢ ((⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)} → (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷) ↔ ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)}))
39	38	biimprcd 251	. . 3 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)} → ((⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷) = {𝑦 ∣ (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐷)} → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷)))
40	36, 37, 39	e10 40592	. 2 ⊢ (   𝐴 ∈ 𝐵   ▶   ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷)   )
41	40	in1 40469	1 ⊢ (𝐴 ∈ 𝐵 → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1520   = wceq 1522   ∈ wcel 2081  {cab 2775  [wsbc 3709  ⦋csb 3815   ∩ cin 3862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-in 3870  df-nul 4216  df-vd1 40468

This theorem is referenced by: (None)