Metamath Proof Explorer


Theorem csbie2df

Description: Conversion of implicit substitution to explicit class substitution. This version of csbiedf avoids a disjointness condition on x , A and x , D by substituting twice. Deduction form of csbie2 . (Contributed by AV, 29-Mar-2024)

Ref Expression
Hypotheses csbie2df.p
|- F/ x ph
csbie2df.c
|- ( ph -> F/_ x C )
csbie2df.d
|- ( ph -> F/_ x D )
csbie2df.a
|- ( ph -> A e. V )
csbie2df.1
|- ( ( ph /\ x = y ) -> B = C )
csbie2df.2
|- ( ( ph /\ y = A ) -> C = D )
Assertion csbie2df
|- ( ph -> [_ A / x ]_ B = D )

Proof

Step Hyp Ref Expression
1 csbie2df.p
 |-  F/ x ph
2 csbie2df.c
 |-  ( ph -> F/_ x C )
3 csbie2df.d
 |-  ( ph -> F/_ x D )
4 csbie2df.a
 |-  ( ph -> A e. V )
5 csbie2df.1
 |-  ( ( ph /\ x = y ) -> B = C )
6 csbie2df.2
 |-  ( ( ph /\ y = A ) -> C = D )
7 eqidd
 |-  ( ph -> D = D )
8 dfsbcq
 |-  ( y = A -> ( [. y / x ]. B = D <-> [. A / x ]. B = D ) )
9 sbceqg
 |-  ( A e. V -> ( [. A / x ]. B = D <-> [_ A / x ]_ B = [_ A / x ]_ D ) )
10 9 adantr
 |-  ( ( A e. V /\ ph ) -> ( [. A / x ]. B = D <-> [_ A / x ]_ B = [_ A / x ]_ D ) )
11 csbtt
 |-  ( ( A e. V /\ F/_ x D ) -> [_ A / x ]_ D = D )
12 3 11 sylan2
 |-  ( ( A e. V /\ ph ) -> [_ A / x ]_ D = D )
13 12 eqeq2d
 |-  ( ( A e. V /\ ph ) -> ( [_ A / x ]_ B = [_ A / x ]_ D <-> [_ A / x ]_ B = D ) )
14 10 13 bitrd
 |-  ( ( A e. V /\ ph ) -> ( [. A / x ]. B = D <-> [_ A / x ]_ B = D ) )
15 4 14 mpancom
 |-  ( ph -> ( [. A / x ]. B = D <-> [_ A / x ]_ B = D ) )
16 8 15 sylan9bb
 |-  ( ( y = A /\ ph ) -> ( [. y / x ]. B = D <-> [_ A / x ]_ B = D ) )
17 16 pm5.74da
 |-  ( y = A -> ( ( ph -> [. y / x ]. B = D ) <-> ( ph -> [_ A / x ]_ B = D ) ) )
18 6 eqeq1d
 |-  ( ( ph /\ y = A ) -> ( C = D <-> D = D ) )
19 18 expcom
 |-  ( y = A -> ( ph -> ( C = D <-> D = D ) ) )
20 19 pm5.74d
 |-  ( y = A -> ( ( ph -> C = D ) <-> ( ph -> D = D ) ) )
21 sbsbc
 |-  ( [ y / x ] B = D <-> [. y / x ]. B = D )
22 2 3 nfeqd
 |-  ( ph -> F/ x C = D )
23 5 eqeq1d
 |-  ( ( ph /\ x = y ) -> ( B = D <-> C = D ) )
24 23 ex
 |-  ( ph -> ( x = y -> ( B = D <-> C = D ) ) )
25 1 22 24 sbiedw
 |-  ( ph -> ( [ y / x ] B = D <-> C = D ) )
26 21 25 bitr3id
 |-  ( ph -> ( [. y / x ]. B = D <-> C = D ) )
27 26 pm5.74i
 |-  ( ( ph -> [. y / x ]. B = D ) <-> ( ph -> C = D ) )
28 17 20 27 vtoclbg
 |-  ( A e. V -> ( ( ph -> [_ A / x ]_ B = D ) <-> ( ph -> D = D ) ) )
29 7 28 mpbiri
 |-  ( A e. V -> ( ph -> [_ A / x ]_ B = D ) )
30 4 29 mpcom
 |-  ( ph -> [_ A / x ]_ B = D )