Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker drex1v if possible. (Contributed by NM, 27-Feb-2005) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | dral1.1 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | drex1 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dral1.1 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | 1 | notbid | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) ) |
| 3 | 2 | dral1 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ¬ 𝜑 ↔ ∀ 𝑦 ¬ 𝜓 ) ) |
| 4 | 3 | notbid | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑦 ¬ 𝜓 ) ) |
| 5 | df-ex | ⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 ) | |
| 6 | df-ex | ⊢ ( ∃ 𝑦 𝜓 ↔ ¬ ∀ 𝑦 ¬ 𝜓 ) | |
| 7 | 4 5 6 | 3bitr4g | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 ) ) |