Metamath Proof Explorer

Theorem bj-sbceqgALT

Description: Distribute proper substitution through an equality relation. Alternate proof of sbceqg . (Contributed by BJ, 6-Oct-2018) Proof modification is discouraged to avoid using sbceqg , but the Metamath program "MM-PA> MINIMIZE__WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dfcleq 
 |-  ( B = C <-> A. y ( y e. B <-> y e. C ) )
2 1 sbcth 
 |-  ( A e. V -> [. A / x ]. ( B = C <-> A. y ( y e. B <-> y e. C ) ) )
3 sbcbig 
 |-  ( A e. V -> ( [. A / x ]. ( B = C <-> A. y ( y e. B <-> y e. C ) ) <-> ( [. A / x ]. B = C <-> [. A / x ]. A. y ( y e. B <-> y e. C ) ) ) )
4 2 3 mpbid 
 |-  ( A e. V -> ( [. A / x ]. B = C <-> [. A / x ]. A. y ( y e. B <-> y e. C ) ) )
5 sbcal 
 |-  ( [. A / x ]. A. y ( y e. B <-> y e. C ) <-> A. y [. A / x ]. ( y e. B <-> y e. C ) )
6 4 5 bitrdi 
 |-  ( A e. V -> ( [. A / x ]. B = C <-> A. y [. A / x ]. ( y e. B <-> y e. C ) ) )
7 sbcbig 
 |-  ( A e. V -> ( [. A / x ]. ( y e. B <-> y e. C ) <-> ( [. A / x ]. y e. B <-> [. A / x ]. y e. C ) ) )
8 7 albidv 
 |-  ( A e. V -> ( A. y [. A / x ]. ( y e. B <-> y e. C ) <-> A. y ( [. A / x ]. y e. B <-> [. A / x ]. y e. C ) ) )
9 sbcel2 
 |-  ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B )
10 9 a1i 
 |-  ( A e. V -> ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) )
11 sbcel2 
 |-  ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C )
12 11 a1i 
 |-  ( A e. V -> ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) )
13 10 12 bibi12d 
 |-  ( A e. V -> ( ( [. A / x ]. y e. B <-> [. A / x ]. y e. C ) <-> ( y e. [_ A / x ]_ B <-> y e. [_ A / x ]_ C ) ) )
14 13 albidv 
 |-  ( A e. V -> ( A. y ( [. A / x ]. y e. B <-> [. A / x ]. y e. C ) <-> A. y ( y e. [_ A / x ]_ B <-> y e. [_ A / x ]_ C ) ) )
15 6 8 14 3bitrd 
 |-  ( A e. V -> ( [. A / x ]. B = C <-> A. y ( y e. [_ A / x ]_ B <-> y e. [_ A / x ]_ C ) ) )
16 dfcleq 
 |-  ( [_ A / x ]_ B = [_ A / x ]_ C <-> A. y ( y e. [_ A / x ]_ B <-> y e. [_ A / x ]_ C ) )
17 15 16 bitr4di 
 |-  ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )