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 | ⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝐴 𝜑 ) |
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 | ⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝐴 𝜑 ) |