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 1970
with two universal quantifiers in the consequent, and
a generalization of hbaevg 1971. One can prove similar statements with
arbitrary numbers of universal quantifiers in the consequent (the series
begins with aeveq 1969, aev 1970, aev2 1973).
Using aev 1970 and alrimiv 1842 (as in aev2ALT 1974), 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 26709. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1713, ax-1 6-- ax-13 2234 (as the one-element universe shows). (Contributed by BJ, 29-Mar-2021.) |
Ref | Expression |
---|---|
aev2 | ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbaevg 1971 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑤 𝑤 = 𝑠) | |
2 | aev 1970 | . 2 ⊢ (∀𝑤 𝑤 = 𝑠 → ∀𝑡 𝑢 = 𝑣) | |
3 | 1, 2 | sylg 1740 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |