Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-nfimexal | Structured version Visualization version GIF version |
Description: A weak from of nonfreeness in either an antecedent or a consequent implies that a universally quantified implication is equivalent to the associated implication where the antecedent is existentially quantified and the consequent is universally quantified. The forward implication always holds (this is 19.38 1846) and the converse implication is the join of instances of bj-alrimg 34494 and bj-exlimg 34498 (see 19.38a 1847 and 19.38b 1848). TODO: prove a version where the antecedents use the nonfreeness quantifier. (Contributed by BJ, 9-Dec-2023.) |
Ref | Expression |
---|---|
bj-nfimexal | ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.38 1846 | . 2 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) | |
2 | bj-alrimg 34494 | . . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) | |
3 | bj-exlimg 34498 | . . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) | |
4 | 2, 3 | jaoi 857 | . 2 ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) |
5 | 1, 4 | impbid2 229 | 1 ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∨ wo 847 ∀wal 1541 ∃wex 1787 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-or 848 df-ex 1788 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |