Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > aev2 | Structured version Visualization version GIF version |
Description: A version of aev 1983
with two universal quantifiers in the consequent, and
a generalization of hbaevg 1984. One can prove similar statements with
arbitrary numbers of universal quantifiers in the consequent (the series
begins with aeveq 1982, aev 1983, aev2 1986).
Using aev 1983 and alrimiv 1855 (as in aev2ALT 1987), one can actually prove (with no more axioms) any scheme of the form (∀𝑥𝑥 = 𝑦 → PHI) , DV (𝑥, 𝑦) where PHI involves only setvar variables and the connectors →, ↔, ∧, ∨, ⊤, =, ∀, ∃, ∃*, ∃!, Ⅎ. An example is given by aevdemo 27317. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1722, ax-1 6-- ax-13 2246 (as the one-element universe shows). (Contributed by BJ, 29-Mar-2021.) |
Ref | Expression |
---|---|
aev2 | ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbaevg 1984 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑤 𝑤 = 𝑠) | |
2 | aev 1983 | . 2 ⊢ (∀𝑤 𝑤 = 𝑠 → ∀𝑡 𝑢 = 𝑣) | |
3 | 1, 2 | sylg 1750 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1481 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |