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

Metamath Proof Explorer

Theorem bnj1476

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1476.1 
|- D = { x e. A | -. ph }
bnj1476.2 
|- ( ps -> D = (/) )
Assertion bnj1476 
|- ( ps -> A. x e. A ph )

Proof

Step Hyp Ref Expression
1 bnj1476.1 
 |-  D = { x e. A | -. ph }
2 bnj1476.2 
 |-  ( ps -> D = (/) )
3 nfrab1 
 |-  F/_ x { x e. A | -. ph }
4 1 3 nfcxfr 
 |-  F/_ x D
5 4 eq0f 
 |-  ( D = (/) <-> A. x -. x e. D )
6 2 5 sylib 
 |-  ( ps -> A. x -. x e. D )
7 1 reqabi 
 |-  ( x e. D <-> ( x e. A /\ -. ph ) )
8 7 notbii 
 |-  ( -. x e. D <-> -. ( x e. A /\ -. ph ) )
9 iman 
 |-  ( ( x e. A -> ph ) <-> -. ( x e. A /\ -. ph ) )
10 8 9 sylbb2 
 |-  ( -. x e. D -> ( x e. A -> ph ) )
11 6 10 sylg 
 |-  ( ps -> A. x ( x e. A -> ph ) )
12 11 bnj1142 
 |-  ( ps -> A. x e. A ph )