This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )