Description: Restricted quantifier version of 19.23v . Version of r19.23 with a disjoint variable condition. (Contributed by NM, 31-Aug-1999) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | r19.23v | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | con34b | ⊢ ( ( 𝜑 → 𝜓 ) ↔ ( ¬ 𝜓 → ¬ 𝜑 ) ) | |
| 2 | 1 | ralbii | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ¬ 𝜓 → ¬ 𝜑 ) ) |
| 3 | r19.21v | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ¬ 𝜓 → ¬ 𝜑 ) ↔ ( ¬ 𝜓 → ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ) | |
| 4 | dfrex2 | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ) | |
| 5 | 4 | imbi1i | ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝜓 ) ↔ ( ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓 ) ) |
| 6 | con1b | ⊢ ( ( ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓 ) ↔ ( ¬ 𝜓 → ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ) | |
| 7 | 5 6 | bitr2i | ⊢ ( ( ¬ 𝜓 → ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝜓 ) ) |
| 8 | 2 3 7 | 3bitri | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → 𝜓 ) ) |