Theorem ralunsn

Description: Restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012) (Revised by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Hypothesis	ralunsn.1	|- ( x = B -> ( ph <-> ps ) )
Assertion	ralunsn	|- ( B e. C -> ( A. x e. ( A u. { B } ) ph <-> ( A. x e. A ph /\ ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		ralunsn.1	|- ( x = B -> ( ph <-> ps ) )
2		ralunb	|- ( A. x e. ( A u. { B } ) ph <-> ( A. x e. A ph /\ A. x e. { B } ph ) )
3	1	ralsng	|- ( B e. C -> ( A. x e. { B } ph <-> ps ) )
4	3	anbi2d	|- ( B e. C -> ( ( A. x e. A ph /\ A. x e. { B } ph ) <-> ( A. x e. A ph /\ ps ) ) )
5	2 4	bitrid	|- ( B e. C -> ( A. x e. ( A u. { B } ) ph <-> ( A. x e. A ph /\ ps ) ) )