Theorem bj-sbeq

Description: Distribute proper substitution through an equality relation. (See sbceqg ). (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-sbeq	|- ( [ y / x ] A = B <-> [_ y / x ]_ A = [_ y / x ]_ B )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	|- ( A = B <-> A. z ( z e. A <-> z e. B ) )
2	1	sbbii	|- ( [ y / x ] A = B <-> [ y / x ] A. z ( z e. A <-> z e. B ) )
3		sbsbc	|- ( [ y / x ] A. z ( z e. A <-> z e. B ) <-> [. y / x ]. A. z ( z e. A <-> z e. B ) )
4		sbcal	|- ( [. y / x ]. A. z ( z e. A <-> z e. B ) <-> A. z [. y / x ]. ( z e. A <-> z e. B ) )
5	2 3 4	3bitri	|- ( [ y / x ] A = B <-> A. z [. y / x ]. ( z e. A <-> z e. B ) )
6		sbcbig	|- ( y e. _V -> ( [. y / x ]. ( z e. A <-> z e. B ) <-> ( [. y / x ]. z e. A <-> [. y / x ]. z e. B ) ) )
7	6	elv	|- ( [. y / x ]. ( z e. A <-> z e. B ) <-> ( [. y / x ]. z e. A <-> [. y / x ]. z e. B ) )
8	7	albii	|- ( A. z [. y / x ]. ( z e. A <-> z e. B ) <-> A. z ( [. y / x ]. z e. A <-> [. y / x ]. z e. B ) )
9		sbcel2	|- ( [. y / x ]. z e. A <-> z e. [_ y / x ]_ A )
10		sbcel2	|- ( [. y / x ]. z e. B <-> z e. [_ y / x ]_ B )
11	9 10	bibi12i	|- ( ( [. y / x ]. z e. A <-> [. y / x ]. z e. B ) <-> ( z e. [_ y / x ]_ A <-> z e. [_ y / x ]_ B ) )
12	11	albii	|- ( A. z ( [. y / x ]. z e. A <-> [. y / x ]. z e. B ) <-> A. z ( z e. [_ y / x ]_ A <-> z e. [_ y / x ]_ B ) )
13	5 8 12	3bitri	|- ( [ y / x ] A = B <-> A. z ( z e. [_ y / x ]_ A <-> z e. [_ y / x ]_ B ) )
14		dfcleq	|- ( [_ y / x ]_ A = [_ y / x ]_ B <-> A. z ( z e. [_ y / x ]_ A <-> z e. [_ y / x ]_ B ) )
15	13 14	bitr4i	|- ( [ y / x ] A = B <-> [_ y / x ]_ A = [_ y / x ]_ B )