Metamath Proof Explorer

Theorem csbiebt

Description: Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf .) (Contributed by NM, 11-Nov-2005)

Ref Expression
Assertion csbiebt 
|- ( ( A e. V /\ F/_ x C ) -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 spsbc 
 |-  ( A e. _V -> ( A. x ( x = A -> B = C ) -> [. A / x ]. ( x = A -> B = C ) ) )
3 2 adantr 
 |-  ( ( A e. _V /\ F/_ x C ) -> ( A. x ( x = A -> B = C ) -> [. A / x ]. ( x = A -> B = C ) ) )
4 simpl 
 |-  ( ( A e. _V /\ F/_ x C ) -> A e. _V )
5 biimt 
 |-  ( x = A -> ( B = C <-> ( x = A -> B = C ) ) )
6 csbeq1a 
 |-  ( x = A -> B = [_ A / x ]_ B )
7 6 eqeq1d 
 |-  ( x = A -> ( B = C <-> [_ A / x ]_ B = C ) )
8 5 7 bitr3d 
 |-  ( x = A -> ( ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
9 8 adantl 
 |-  ( ( ( A e. _V /\ F/_ x C ) /\ x = A ) -> ( ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
10 nfv 
 |-  F/ x A e. _V
11 nfnfc1 
 |-  F/ x F/_ x C
12 10 11 nfan 
 |-  F/ x ( A e. _V /\ F/_ x C )
13 nfcsb1v 
 |-  F/_ x [_ A / x ]_ B
14 13 a1i 
 |-  ( ( A e. _V /\ F/_ x C ) -> F/_ x [_ A / x ]_ B )
15 simpr 
 |-  ( ( A e. _V /\ F/_ x C ) -> F/_ x C )
16 14 15 nfeqd 
 |-  ( ( A e. _V /\ F/_ x C ) -> F/ x [_ A / x ]_ B = C )
17 4 9 12 16 sbciedf 
 |-  ( ( A e. _V /\ F/_ x C ) -> ( [. A / x ]. ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
18 3 17 sylibd 
 |-  ( ( A e. _V /\ F/_ x C ) -> ( A. x ( x = A -> B = C ) -> [_ A / x ]_ B = C ) )
19 13 a1i 
 |-  ( F/_ x C -> F/_ x [_ A / x ]_ B )
20 id 
 |-  ( F/_ x C -> F/_ x C )
21 19 20 nfeqd 
 |-  ( F/_ x C -> F/ x [_ A / x ]_ B = C )
22 11 21 nfan1 
 |-  F/ x ( F/_ x C /\ [_ A / x ]_ B = C )
23 7 biimprcd 
 |-  ( [_ A / x ]_ B = C -> ( x = A -> B = C ) )
24 23 adantl 
 |-  ( ( F/_ x C /\ [_ A / x ]_ B = C ) -> ( x = A -> B = C ) )
25 22 24 alrimi 
 |-  ( ( F/_ x C /\ [_ A / x ]_ B = C ) -> A. x ( x = A -> B = C ) )
26 25 ex 
 |-  ( F/_ x C -> ( [_ A / x ]_ B = C -> A. x ( x = A -> B = C ) ) )
27 26 adantl 
 |-  ( ( A e. _V /\ F/_ x C ) -> ( [_ A / x ]_ B = C -> A. x ( x = A -> B = C ) ) )
28 18 27 impbid 
 |-  ( ( A e. _V /\ F/_ x C ) -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )
29 1 28 sylan 
 |-  ( ( A e. V /\ F/_ x C ) -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )