Description: Obsolete version of ceqsexv as of 12-Oct-2024. (Contributed by NM, 2-Mar-1995) Avoid ax-12 . (Revised by Gino Giotto, 12-Oct-2024) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ceqsexvOLD.1 | ⊢ 𝐴 ∈ V | |
| ceqsexvOLD.2 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | ||
| Assertion | ceqsexvOLD | ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ceqsexvOLD.1 | ⊢ 𝐴 ∈ V | |
| 2 | ceqsexvOLD.2 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
| 3 | 2 | biimpa | ⊢ ( ( 𝑥 = 𝐴 ∧ 𝜑 ) → 𝜓 ) |
| 4 | 3 | exlimiv | ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) → 𝜓 ) |
| 5 | 2 | biimprcd | ⊢ ( 𝜓 → ( 𝑥 = 𝐴 → 𝜑 ) ) |
| 6 | 5 | alrimiv | ⊢ ( 𝜓 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) |
| 7 | 1 | isseti | ⊢ ∃ 𝑥 𝑥 = 𝐴 |
| 8 | exintr | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) → ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ) | |
| 9 | 6 7 8 | mpisyl | ⊢ ( 𝜓 → ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) |
| 10 | 4 9 | impbii | ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 ) |