Description: The extension of a predicate ( ph ( z ) ) is included in a set ( x ) if and only if it is a set ( y ). Sufficiency is obvious, and necessity is the content of the axiom of separation ax-sep . Similar to Theorem 1.3(ii) of BellMachover p. 463. (Contributed by NM, 21-Jun-1993) Generalized to a closed form biconditional with existential quantifications using two different setvars x , y (which need not be disjoint). (Revised by BJ, 8-Aug-2022)
TODO: move in place of bm1.3ii . Relabel ("sepbi"?).
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-bm1.3ii | ⊢ ( ∃ 𝑥 ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑥 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elequ2 | ⊢ ( 𝑥 = 𝑡 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑡 ) ) | |
| 2 | 1 | imbi2d | ⊢ ( 𝑥 = 𝑡 → ( ( 𝜑 → 𝑧 ∈ 𝑥 ) ↔ ( 𝜑 → 𝑧 ∈ 𝑡 ) ) ) |
| 3 | 2 | albidv | ⊢ ( 𝑥 = 𝑡 → ( ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) ) ) |
| 4 | 3 | cbvexvw | ⊢ ( ∃ 𝑥 ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑥 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) ) |
| 5 | ax-sep | ⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑡 ∧ 𝜑 ) ) | |
| 6 | 19.42v | ⊢ ( ∃ 𝑦 ( ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑡 ∧ 𝜑 ) ) ) ↔ ( ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) ∧ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑡 ∧ 𝜑 ) ) ) ) | |
| 7 | bimsc1 | ⊢ ( ( ( 𝜑 → 𝑧 ∈ 𝑡 ) ∧ ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑡 ∧ 𝜑 ) ) ) → ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ) | |
| 8 | 7 | alanimi | ⊢ ( ( ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑡 ∧ 𝜑 ) ) ) → ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ) |
| 9 | 8 | eximi | ⊢ ( ∃ 𝑦 ( ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ) |
| 10 | 6 9 | sylbir | ⊢ ( ( ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) ∧ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ) |
| 11 | 5 10 | mpan2 | ⊢ ( ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ) |
| 12 | 11 | exlimiv | ⊢ ( ∃ 𝑡 ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ) |
| 13 | elequ2 | ⊢ ( 𝑦 = 𝑡 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑡 ) ) | |
| 14 | 13 | bibi1d | ⊢ ( 𝑦 = 𝑡 → ( ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ↔ ( 𝑧 ∈ 𝑡 ↔ 𝜑 ) ) ) |
| 15 | 14 | albidv | ⊢ ( 𝑦 = 𝑡 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ 𝜑 ) ) ) |
| 16 | 15 | cbvexvw | ⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ 𝜑 ) ) |
| 17 | biimpr | ⊢ ( ( 𝑧 ∈ 𝑡 ↔ 𝜑 ) → ( 𝜑 → 𝑧 ∈ 𝑡 ) ) | |
| 18 | 17 | alimi | ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ 𝜑 ) → ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) ) |
| 19 | 18 | eximi | ⊢ ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ 𝜑 ) → ∃ 𝑡 ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) ) |
| 20 | 16 19 | sylbi | ⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) → ∃ 𝑡 ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) ) |
| 21 | 12 20 | impbii | ⊢ ( ∃ 𝑡 ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑡 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ) |
| 22 | 4 21 | bitri | ⊢ ( ∃ 𝑥 ∀ 𝑧 ( 𝜑 → 𝑧 ∈ 𝑥 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ 𝜑 ) ) |