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 𝐷 = { 𝑥𝐴 ∣ ¬ 𝜑 }
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 rabeq2i ( 𝑥𝐷 ↔ ( 𝑥𝐴 ∧ ¬ 𝜑 ) )
8 7 notbii ( ¬ 𝑥𝐷 ↔ ¬ ( 𝑥𝐴 ∧ ¬ 𝜑 ) )
9 iman ( ( 𝑥𝐴𝜑 ) ↔ ¬ ( 𝑥𝐴 ∧ ¬ 𝜑 ) )
10 8 9 sylbb2 ( ¬ 𝑥𝐷 → ( 𝑥𝐴𝜑 ) )
11 6 10 sylg ( 𝜓 → ∀ 𝑥 ( 𝑥𝐴𝜑 ) )
12 11 bnj1142 ( 𝜓 → ∀ 𝑥𝐴 𝜑 )