Theorem clelsb2

Description: Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 ). (Contributed by Jim Kingdon, 22-Nov-2018)

	Ref	Expression
Assertion	clelsb2	|- ( [ y / x ] A e. x <-> A e. y )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ x A e. w
2	1	sbco2	|- ( [ y / x ] [ x / w ] A e. w <-> [ y / w ] A e. w )
3		nfv	|- F/ w A e. x
4		eleq2	|- ( w = x -> ( A e. w <-> A e. x ) )
5	3 4	sbie	|- ( [ x / w ] A e. w <-> A e. x )
6	5	sbbii	|- ( [ y / x ] [ x / w ] A e. w <-> [ y / x ] A e. x )
7		nfv	|- F/ w A e. y
8		eleq2	|- ( w = y -> ( A e. w <-> A e. y ) )
9	7 8	sbie	|- ( [ y / w ] A e. w <-> A e. y )
10	2 6 9	3bitr3i	|- ( [ y / x ] A e. x <-> A e. y )