Description: Obsolete version of eqabb as of 12-Feb-2025. (Contributed by NM, 26-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eqabbOLD | ⊢ ( 𝐴 = { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-5 | ⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 ) | |
| 2 | hbab1 | ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ∀ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) | |
| 3 | 1 2 | cleqh | ⊢ ( 𝐴 = { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑥 ∣ 𝜑 } ) ) |
| 4 | abid | ⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 ) | |
| 5 | 4 | bibi2i | ⊢ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ( 𝑥 ∈ 𝐴 ↔ 𝜑 ) ) |
| 6 | 5 | albii | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝜑 ) ) |
| 7 | 3 6 | bitri | ⊢ ( 𝐴 = { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝜑 ) ) |