This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )