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=\left\{x\in A|\neg \phi \right\}$$
	bnj1476.2	$$⊢\psi \to D=\varnothing$$
Assertion	bnj1476	$$⊢\psi \to \forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		bnj1476.1	$$⊢D=\left\{x\in A|\neg \phi \right\}$$
2		bnj1476.2	$$⊢\psi \to D=\varnothing$$
3		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|\neg \phi \right\}$$
4	1 3	nfcxfr	$$⊢\underset{\_}{Ⅎ}xD$$
5	4	eq0f	$$⊢D=\varnothing \leftrightarrow \forall x\neg x\in D$$
6	2 5	sylib	$$⊢\psi \to \forall x\neg x\in D$$
7	1	reqabi	$$⊢x\in D\leftrightarrow \left(x\in A\wedge \neg \phi \right)$$
8	7	notbii	$$⊢\neg x\in D\leftrightarrow \neg \left(x\in A\wedge \neg \phi \right)$$
9		iman	$$⊢\left(x\in A\to \phi \right)\leftrightarrow \neg \left(x\in A\wedge \neg \phi \right)$$
10	8 9	sylbb2	$$⊢\neg x\in D\to \left(x\in A\to \phi \right)$$
11	6 10	sylg	$$⊢\psi \to \forall x\left(x\in A\to \phi \right)$$
12	11	ralrid	$$⊢\psi \to \forall x\in A\phi$$