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 1839) and the converse implication is the join of instances of bj-alrimg 33952 and bj-exlimg 33956 (see 19.38a 1840 and 19.38b 1841). 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 1839 | . 2 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) | |
2 | bj-alrimg 33952 | . . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) | |
3 | bj-exlimg 33956 | . . 3 ⊢ ((∃𝑥𝜓 → ∀𝑥𝜓) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) | |
4 | 2, 3 | jaoi 853 | . 2 ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))) |
5 | 1, 4 | impbid2 228 | 1 ⊢ (((∃𝑥𝜑 → ∀𝑥𝜑) ∨ (∃𝑥𝜓 → ∀𝑥𝜓)) → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∨ wo 843 ∀wal 1535 ∃wex 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
This theorem depends on definitions: df-bi 209 df-or 844 df-ex 1781 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |