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