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 2007
with two universal quantifiers in the consequent, and
a generalization of hbaevg 2008. One can prove similar statements with
arbitrary numbers of universal quantifiers in the consequent (the series
begins with aeveq 2006, aev 2007, aev2 2013).
Using aev 2007 and alrimiv 1887 (as in aev2ALT 2014), 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 28032. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1759, ax-1 6-- ax-13 2302 (as the one-element universe shows). (Contributed by BJ, 29-Mar-2021.) |
Ref | Expression |
---|---|
aev2 | ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbaevg 2008 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑤 𝑤 = 𝑠) | |
2 | aev 2007 | . 2 ⊢ (∀𝑤 𝑤 = 𝑠 → ∀𝑡 𝑢 = 𝑣) | |
3 | 1, 2 | sylg 1786 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1506 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1744 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |