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

Metamath Proof Explorer

Theorem raldifsnb

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

Ref Expression
Assertion raldifsnb 
|- ( A. x e. A ( x =/= Y -> ph ) <-> A. x e. ( A \ { Y } ) ph )

Proof

Step Hyp Ref Expression
1 velsn 
 |-  ( x e. { Y } <-> x = Y )
2 nnel 
 |-  ( -. x e/ { Y } <-> x e. { Y } )
3 nne 
 |-  ( -. x =/= Y <-> x = Y )
4 1 2 3 3bitr4ri 
 |-  ( -. x =/= Y <-> -. x e/ { Y } )
5 4 con4bii 
 |-  ( x =/= Y <-> x e/ { Y } )
6 5 imbi1i 
 |-  ( ( x =/= Y -> ph ) <-> ( x e/ { Y } -> ph ) )
7 6 ralbii 
 |-  ( A. x e. A ( x =/= Y -> ph ) <-> A. x e. A ( x e/ { Y } -> ph ) )
8 raldifb 
 |-  ( A. x e. A ( x e/ { Y } -> ph ) <-> A. x e. ( A \ { Y } ) ph )
9 7 8 bitri 
 |-  ( A. x e. A ( x =/= Y -> ph ) <-> A. x e. ( A \ { Y } ) ph )