Description: A variable not free in a wff remains so in a restricted class abstraction. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfrabw when possible. (Contributed by NM, 13-Oct-2003) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfrab.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| nfrab.2 | ⊢ Ⅎ 𝑥 𝐴 | ||
| Assertion | nfrab | ⊢ Ⅎ 𝑥 { 𝑦 ∈ 𝐴 ∣ 𝜑 } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfrab.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| 2 | nfrab.2 | ⊢ Ⅎ 𝑥 𝐴 | |
| 3 | df-rab | ⊢ { 𝑦 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } | |
| 4 | nftru | ⊢ Ⅎ 𝑦 ⊤ | |
| 5 | 2 | nfcri | ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴 |
| 6 | eleq1w | ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) ) | |
| 7 | 5 6 | dvelimnf | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 ∈ 𝐴 ) |
| 8 | 1 | a1i | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 ) |
| 9 | 7 8 | nfand | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ) |
| 10 | 9 | adantl | ⊢ ( ( ⊤ ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ) |
| 11 | 4 10 | nfabd2 | ⊢ ( ⊤ → Ⅎ 𝑥 { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } ) |
| 12 | 11 | mptru | ⊢ Ⅎ 𝑥 { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } |
| 13 | 3 12 | nfcxfr | ⊢ Ⅎ 𝑥 { 𝑦 ∈ 𝐴 ∣ 𝜑 } |