Metamath Proof Explorer

Theorem csbfv12gALTVD

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

1:: |- (. A e. C ->. A e. C ).
2:1: |- (. A e. C ->. [_ A / x ]_ { y } = { y } ).
3:1: |- (. A e. C ->. [_ A / x ]_ ( F " { B } ) = ( [_ A / x ]_ F " [_ A / x ]_ { B } ) ).
4:1: |- (. A e. C ->. [_ A / x ]_ { B } = { [_ A / x ]_ B } ).
5:4: |- (. A e. C ->. ( [_ A / x ]_ F " [_ A / x ]_ { B } ) = ( [_ A / x ]_ F " { [_ A / x ]_ B } ) ).
6:3,5: |- (. A e. C ->. [_ A / x ]_ ( F " { B } ) = ( [_ A / x ]_ F " { [_ A / x ]_ B } ) ).
7:1: |- (. A e. C ->. ( [. A / x ]. ( F " { B } ) = { y } <-> [_ A / x ]_ ( F " { B } ) = [_ A / x ]_ { y } ) ).
8:6,2: |- (. A e. C ->. ( [_ A / x ]_ ( F " { B } ) = [_ A / x ]_ { y } <-> ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } ) ).
9:7,8: |- (. A e. C ->. ( [. A / x ]. ( F " { B } ) = { y } <-> ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } ) ).
10:9: |- (. A e. C ->. A. y ( [. A / x ]. ( F " { B } ) = { y } <-> ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } ) ).
11:10: |- (. A e. C ->. { y | [. A / x ]. ( F " { B } ) = { y } } = { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
12:1: |- (. A e. C ->. [_ A / x ]_ { y | ( F " { B } ) = { y } } = { y | [. A / x ]. ( F " { B } ) = { y } } ).
13:11,12: |- (. A e. C ->. [_ A / x ]_ { y | ( F " { B } ) = { y } } = { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
14:13: |- (. A e. C ->. U. [_ A / x ]_ { y | ( F " { B } ) = { y } } = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
15:1: |- (. A e. C ->. [_ A / x ]_ U. { y | ( F " { B } ) = { y } } = U. [_ A / x ]_ { y | ( F " { B } ) = { y } } ).
16:14,15: |- (. A e. C ->. [_ A / x ]_ U. { y | ( F " { B } ) = { y } } = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
17:: |- ( FB ) = U. { y | ( F " { B } ) = { y } }
18:17: |- A. x ( FB ) = U. { y | ( F " { B } ) = { y } }
19:1,18: |- (. A e. C ->. [_ A / x ]_ ( FB ) = [_ A / x ]_ U. { y | ( F " { B } ) = { y } } ).
20:16,19: |- (. A e. C ->. [_ A / x ]_ ( FB ) = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
21:: |- ( [_ A / x ]_ F[_ A / x ]_ B ) = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } }
22:20,21: |- (. A e. C ->. [_ A / x ]_ ( FB ) = ( [_ A / x ]_ F[_ A / x ]_ B ) ).
qed:22: |- ( A e. C -> [_ A / x ]_ ( FB ) = ( [_ A / x ]_ F[_ A / x ]_ B ) )
(Contributed by Alan Sare, 10-Nov-2012) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 idn1 ⊢ (    𝐴 ∈ 𝐶    ▶    𝐴 ∈ 𝐶    )
2 sbceqg ⊢ ( 𝐴 ∈ 𝐶 → ( [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } ) )
3 1 2 e1a ⊢ (    𝐴 ∈ 𝐶    ▶    ( [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } )    )
4 csbima12 ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } )
5 4 a1i ⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } ) )
6 1 5 e1a ⊢ (    𝐴 ∈ 𝐶    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } )    )
7 csbsng ⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } = { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )
8 1 7 e1a ⊢ (    𝐴 ∈ 𝐶    ▶    ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } = { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }    )
9 imaeq2 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } = { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) )
10 8 9 e1a ⊢ (    𝐴 ∈ 𝐶    ▶    ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )    )
11 eqeq1 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } ) → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) ) )
12 11 biimprd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } ) → ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) ) )
13 6 10 12 e11 ⊢ (    𝐴 ∈ 𝐶    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } )    )
14 csbconstg ⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } = { 𝑦 } )
15 1 14 e1a ⊢ (    𝐴 ∈ 𝐶    ▶    ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } = { 𝑦 }    )
16 eqeq12 ⊢ ( ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) ∧ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } = { 𝑦 } ) → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } ) )
17 16 ex ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } = { 𝑦 } → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } ) ) )
18 13 15 17 e11 ⊢ (    𝐴 ∈ 𝐶    ▶    ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } )    )
19 bibi1 ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } ) → ( ( [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } ) ↔ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } ) ) )
20 19 biimprd ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } ) → ( ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 “ { 𝐵 } ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 } ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } ) → ( [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } ) ) )
21 3 18 20 e11 ⊢ (    𝐴 ∈ 𝐶    ▶    ( [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } )    )
22 21 gen11 ⊢ (    𝐴 ∈ 𝐶    ▶    ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } )    )
23 abbi ⊢ ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } ) ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } )
24 23 biimpi ⊢ ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } ) → { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } )
25 22 24 e1a ⊢ (    𝐴 ∈ 𝐶    ▶    { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } }    )
26 csbab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } }
27 26 a1i ⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } )
28 1 27 e1a ⊢ (    𝐴 ∈ 𝐶    ▶    ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } }    )
29 eqeq2 ⊢ ( { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } ↔ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } ) )
30 29 biimpd ⊢ ( { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } → ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } ) )
31 25 28 30 e11 ⊢ (    𝐴 ∈ 𝐶    ▶    ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } }    )
32 unieq ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } → ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } )
33 31 32 e1a ⊢ (    𝐴 ∈ 𝐶    ▶    ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } }    )
34 csbuni ⊢ ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } }
35 34 a1i ⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } )
36 1 35 e1a ⊢ (    𝐴 ∈ 𝐶    ▶    ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } }    )
37 eqeq2 ⊢ ( ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } → ( ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } ↔ ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } ) )
38 37 biimpd ⊢ ( ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } → ( ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } → ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } ) )
39 33 36 38 e11 ⊢ (    𝐴 ∈ 𝐶    ▶    ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } }    )
40 dffv4 ⊢ ( 𝐹 ‘ 𝐵 ) = ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } }
41 40 ax-gen ⊢ ∀ 𝑥 ( 𝐹 ‘ 𝐵 ) = ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } }
42 csbeq2 ⊢ ( ∀ 𝑥 ( 𝐹 ‘ 𝐵 ) = ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } )
43 42 a1i ⊢ ( 𝐴 ∈ 𝐶 → ( ∀ 𝑥 ( 𝐹 ‘ 𝐵 ) = ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } ) )
44 1 41 43 e10 ⊢ (    𝐴 ∈ 𝐶    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } }    )
45 eqeq2 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } ) )
46 45 biimpd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑦 ∣ ( 𝐹 “ { 𝐵 } ) = { 𝑦 } } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } ) )
47 39 44 46 e11 ⊢ (    𝐴 ∈ 𝐶    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } }    )
48 dffv4 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } }
49 eqeq2 ⊢ ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } ) )
50 49 biimprcd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } → ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) = ∪ { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝐵 } ) = { 𝑦 } } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
51 47 48 50 e10 ⊢ (    𝐴 ∈ 𝐶    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )    )
52 51 in1 ⊢ ( 𝐴 ∈ 𝐶 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ 𝐵 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )