Theorem raldifeq

Description: Equality theorem for restricted universal quantifier. (Contributed by Thierry Arnoux, 6-Jul-2019)

	Ref	Expression
Hypotheses	raldifeq.1	|- ( ph -> A C_ B )
	raldifeq.2	|- ( ph -> A. x e. ( B \ A ) ps )
Assertion	raldifeq	|- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )

Proof

Step	Hyp	Ref	Expression
1		raldifeq.1	|- ( ph -> A C_ B )
2		raldifeq.2	|- ( ph -> A. x e. ( B \ A ) ps )
3	2	biantrud	|- ( ph -> ( A. x e. A ps <-> ( A. x e. A ps /\ A. x e. ( B \ A ) ps ) ) )
4		ralunb	|- ( A. x e. ( A u. ( B \ A ) ) ps <-> ( A. x e. A ps /\ A. x e. ( B \ A ) ps ) )
5	3 4	bitr4di	|- ( ph -> ( A. x e. A ps <-> A. x e. ( A u. ( B \ A ) ) ps ) )
6		undif	|- ( A C_ B <-> ( A u. ( B \ A ) ) = B )
7	1 6	sylib	|- ( ph -> ( A u. ( B \ A ) ) = B )
8	7	raleqdv	|- ( ph -> ( A. x e. ( A u. ( B \ A ) ) ps <-> A. x e. B ps ) )
9	5 8	bitrd	|- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )