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	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 }
	bnj1476.2	⊢ ( 𝜓 → 𝐷 = ∅ )
Assertion	bnj1476	⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		bnj1476.1	⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 }
2		bnj1476.2	⊢ ( 𝜓 → 𝐷 = ∅ )
3		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 }
4	1 3	nfcxfr	⊢ Ⅎ 𝑥 𝐷
5	4	eq0f	⊢ ( 𝐷 = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ 𝐷 )
6	2 5	sylib	⊢ ( 𝜓 → ∀ 𝑥 ¬ 𝑥 ∈ 𝐷 )
7	1	reqabi	⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) )
8	7	notbii	⊢ ( ¬ 𝑥 ∈ 𝐷 ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) )
9		iman	⊢ ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) )
10	8 9	sylbb2	⊢ ( ¬ 𝑥 ∈ 𝐷 → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
11	6 10	sylg	⊢ ( 𝜓 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
12	11	ralrid	⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝐴 𝜑 )