Description: A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction belongs to variable. (Contributed by BJ, 30-Apr-2024) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eliminable-abelv | ⊢ ( { 𝑥 ∣ 𝜑 } ∈ 𝑦 ↔ ∃ 𝑧 ( ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ∧ 𝑧 ∈ 𝑦 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfclel | ⊢ ( { 𝑥 ∣ 𝜑 } ∈ 𝑦 ↔ ∃ 𝑧 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ) | |
| 2 | eliminable-veqab | ⊢ ( 𝑧 = { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ) | |
| 3 | 2 | anbi1i | ⊢ ( ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ∧ 𝑧 ∈ 𝑦 ) ) |
| 4 | 3 | exbii | ⊢ ( ∃ 𝑧 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑧 ( ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ∧ 𝑧 ∈ 𝑦 ) ) |
| 5 | 1 4 | bitri | ⊢ ( { 𝑥 ∣ 𝜑 } ∈ 𝑦 ↔ ∃ 𝑧 ( ∀ 𝑡 ( 𝑡 ∈ 𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ∧ 𝑧 ∈ 𝑦 ) ) |