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 2067
with two universal quantifiers in the consequent.
One can prove similar statements with arbitrary numbers of universal
quantifiers in the consequent (the series begins with aeveq 2066, aev 2067,
aev2 2068).
Using aev 2067 and alrimiv 1934, 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 28397. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1802, ax-1 6-- ax-13 2372 (as the one-element universe shows). (Contributed by BJ, 23-Mar-2021.) |
Ref | Expression |
---|---|
aev2 | ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aev 2067 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑤 𝑤 = 𝑠) | |
2 | aev 2067 | . . 3 ⊢ (∀𝑤 𝑤 = 𝑠 → ∀𝑡 𝑢 = 𝑣) | |
3 | 2 | alrimiv 1934 | . 2 ⊢ (∀𝑤 𝑤 = 𝑠 → ∀𝑧∀𝑡 𝑢 = 𝑣) |
4 | 1, 3 | syl 17 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 |
This theorem is referenced by: hbaev 2069 |
Copyright terms: Public domain | W3C validator |