Description: Obsolete proof of abbi as of 7-Jan-2024. (Contributed by NM, 25-Nov-2013) (Revised by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 16-Nov-2019) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | abbiOLD | ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hbab1 | ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ∀ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) | |
| 2 | hbab1 | ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } → ∀ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) | |
| 3 | 1 2 | cleqh | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑥 ∈ { 𝑥 ∣ 𝜓 } ) ) |
| 4 | abid | ⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 ) | |
| 5 | abid | ⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜓 ) | |
| 6 | 4 5 | bibi12i | ⊢ ( ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑥 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ( 𝜑 ↔ 𝜓 ) ) |
| 7 | 6 | albii | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑥 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ) |
| 8 | 3 7 | bitr2i | ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ) |