Theorem csbfv12gALTVD 45349

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

1::	⊢ (   𝐴 ∈ 𝐶   ▶   𝐴 ∈ 𝐶   )
2:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝑦} = { 𝑦}   )
3:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵 }) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵})   )
4:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = { ⦋𝐴 / 𝑥⦌𝐵}   )
5:4:	⊢ (   𝐴 ∈ 𝐶   ▶   (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵})   )
6:3,5:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵 }) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵})   )
7:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ([𝐴 / 𝑥](𝐹 “ { 𝐵}) = {𝑦} ↔ ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦})   )
8:6,2:	⊢ (   𝐴 ∈ 𝐶   ▶   (⦋𝐴 / 𝑥⦌(𝐹 “ { 𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})   )
9:7,8:	⊢ (   𝐴 ∈ 𝐶   ▶   ([𝐴 / 𝑥](𝐹 “ { 𝐵}) = {𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})    )
10:9:	⊢ (   𝐴 ∈ 𝐶   ▶   ∀𝑦([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})   )
11:10:	⊢ (   𝐴 ∈ 𝐶   ▶   {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
12:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}}   )
13:11,12:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦 }}   )
14:13:	⊢ (   𝐴 ∈ 𝐶   ▶   ∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ ( 𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
15:1:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ ( 𝐹 “ {𝐵}) = {𝑦}} = ∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}   )
16:14,15:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ ( 𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
17::	⊢ (𝐹‘𝐵) = ∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}
18:17:	⊢ ∀𝑥(𝐹‘𝐵) = ∪ {𝑦 ∣ (𝐹 “ {𝐵 }) = {𝑦}}
19:1,18:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}   )
20:16,19:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
21::	⊢ (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}
22:20,21:	⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵)   )
qed:22:	⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵))

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

Assertion

Ref	Expression
csbfv12gALTVD	⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵))

Proof of Theorem csbfv12gALTVD

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn1 45025	. . . . . . . . . . 11 ⊢ (   𝐴 ∈ 𝐶   ▶   𝐴 ∈ 𝐶   )
2		sbceqg 4347	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝐶 → ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦}))
3	1, 2	e1a 45078	. . . . . . . . . 10 ⊢ (   𝐴 ∈ 𝐶   ▶   ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦})   )
4		csbima12 6038	. . . . . . . . . . . . . 14 ⊢ ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵})
5	4	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵}))
6	1, 5	e1a 45078	. . . . . . . . . . . 12 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵})   )
7		csbsng 4647	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵})
8	1, 7	e1a 45078	. . . . . . . . . . . . 13 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵}   )
9		imaeq2 6015	. . . . . . . . . . . . 13 ⊢ (⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}))
10	8, 9	e1a 45078	. . . . . . . . . . . 12 ⊢ (   𝐴 ∈ 𝐶   ▶   (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵})   )
11		eqeq1 2744	. . . . . . . . . . . . 13 ⊢ (⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵}) → (⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) ↔ (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵})))
12	11	biimprd 249	. . . . . . . . . . . 12 ⊢ (⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵}) → ((⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) → ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵})))
13	6, 10, 12	e11 45139	. . . . . . . . . . 11 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵})   )
14		csbconstg 3857	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌{𝑦} = {𝑦})
15	1, 14	e1a 45078	. . . . . . . . . . 11 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝑦} = {𝑦}   )
16		eqeq12 2757	. . . . . . . . . . . 12 ⊢ ((⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) ∧ ⦋𝐴 / 𝑥⦌{𝑦} = {𝑦}) → (⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}))
17	16	ex 413	. . . . . . . . . . 11 ⊢ (⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) → (⦋𝐴 / 𝑥⦌{𝑦} = {𝑦} → (⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})))
18	13, 15, 17	e11 45139	. . . . . . . . . 10 ⊢ (   𝐴 ∈ 𝐶   ▶   (⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})   )
19		bibi1 352	. . . . . . . . . . 11 ⊢ (([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦}) → (([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}) ↔ (⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})))
20	19	biimprd 249	. . . . . . . . . 10 ⊢ (([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦}) → ((⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}) → ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})))
21	3, 18, 20	e11 45139	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝐶   ▶   ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})   )
22	21	gen11 45067	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝐶   ▶   ∀𝑦([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})   )
23		abbib 2809	. . . . . . . . 9 ⊢ ({𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} ↔ ∀𝑦([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}))
24	23	biimpri 229	. . . . . . . 8 ⊢ (∀𝑦([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}) → {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}})
25	22, 24	e1a 45078	. . . . . . 7 ⊢ (   𝐴 ∈ 𝐶   ▶   {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
26		csbab 4375	. . . . . . . . 9 ⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}}
27	26	a1i 11	. . . . . . . 8 ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}})
28	1, 27	e1a 45078	. . . . . . 7 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}}   )
29		eqeq2 2752	. . . . . . . 8 ⊢ ({𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} → (⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} ↔ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}))
30	29	biimpd 230	. . . . . . 7 ⊢ ({𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} → (⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} → ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}))
31	25, 28, 30	e11 45139	. . . . . 6 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
32		unieq 4856	. . . . . 6 ⊢ (⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} → ∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}})
33	31, 32	e1a 45078	. . . . 5 ⊢ (   𝐴 ∈ 𝐶   ▶   ∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
34		csbuni 4875	. . . . . . 7 ⊢ ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}
35	34	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}})
36	1, 35	e1a 45078	. . . . 5 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}   )
37		eqeq2 2752	. . . . . 6 ⊢ (∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} → (⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} ↔ ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}))
38	37	biimpd 230	. . . . 5 ⊢ (∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} → (⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}))
39	33, 36, 38	e11 45139	. . . 4 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
40		dffv4 6831	. . . . . 6 ⊢ (𝐹‘𝐵) = ∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}
41	40	ax-gen 1802	. . . . 5 ⊢ ∀𝑥(𝐹‘𝐵) = ∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}
42		csbeq2 3843	. . . . . 6 ⊢ (∀𝑥(𝐹‘𝐵) = ∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}})
43	42	a1i 11	. . . . 5 ⊢ (𝐴 ∈ 𝐶 → (∀𝑥(𝐹‘𝐵) = ∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}))
44	1, 41, 43	e10 45145	. . . 4 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}   )
45		eqeq2 2752	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} → (⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} ↔ ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}))
46	45	biimpd 230	. . . 4 ⊢ (⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} → (⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ⦋𝐴 / 𝑥⦌∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}))
47	39, 44, 46	e11 45139	. . 3 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}   )
48		dffv4 6831	. . 3 ⊢ (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}
49		eqeq2 2752	. . . 4 ⊢ ((⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} → (⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵) ↔ ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}))
50	49	biimprcd 251	. . 3 ⊢ (⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} → ((⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵)))
51	47, 48, 50	e10 45145	. 2 ⊢ (   𝐴 ∈ 𝐶   ▶   ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵)   )
52	51	in1 45022	1 ⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   = wceq 1547   ∈ wcel 2119  {cab 2718  [wsbc 3730  ⦋csb 3838  {csn 4562  ∪ cuni 4845   “ cima 5628  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fv 6500  df-vd1 45021

This theorem is referenced by: (None)