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

Metamath Proof Explorer

Theorem raldifb

Description: Restricted universal quantification on a class difference in terms of an implication. (Contributed by Alexander van der Vekens, 3-Jan-2018)

Ref Expression
Assertion raldifb 
|- ( A. x e. A ( x e/ B -> ph ) <-> A. x e. ( A \ B ) ph )

Proof

Step Hyp Ref Expression
1 impexp 
 |-  ( ( ( x e. A /\ x e/ B ) -> ph ) <-> ( x e. A -> ( x e/ B -> ph ) ) )
2 df-nel 
 |-  ( x e/ B <-> -. x e. B )
3 2 anbi2i 
 |-  ( ( x e. A /\ x e/ B ) <-> ( x e. A /\ -. x e. B ) )
4 eldif 
 |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
5 3 4 bitr4i 
 |-  ( ( x e. A /\ x e/ B ) <-> x e. ( A \ B ) )
6 5 imbi1i 
 |-  ( ( ( x e. A /\ x e/ B ) -> ph ) <-> ( x e. ( A \ B ) -> ph ) )
7 1 6 bitr3i 
 |-  ( ( x e. A -> ( x e/ B -> ph ) ) <-> ( x e. ( A \ B ) -> ph ) )
8 7 ralbii2 
 |-  ( A. x e. A ( x e/ B -> ph ) <-> A. x e. ( A \ B ) ph )