Description: A version of aev 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 , aev , aev2 ).
Using aev and alrimiv , one can actually prove (with no more axioms) any scheme of the form ( A. x x = y -> PHI) , DV ( x , y ) where PHI involves only setvar variables and the connectors -> , <-> , /\ , \/ , T. , = , A. , E. , E* , E! , F/ . An example is given by aevdemo . This list cannot be extended to -. or F. since the scheme A. x x = y is consistent with ax-mp , ax-gen , ax-1 -- ax-13 (as the one-element universe shows), so for instance ( A. x x = y -> F. ) , DV ( x , y ) is not provable from these axioms alone (indeed, dtru uses non-logical axioms as well). (Contributed by BJ, 23-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | aev2 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 ∀ 𝑡 𝑢 = 𝑣 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aev | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑤 𝑤 = 𝑠 ) | |
2 | aev | ⊢ ( ∀ 𝑤 𝑤 = 𝑠 → ∀ 𝑡 𝑢 = 𝑣 ) | |
3 | 2 | alrimiv | ⊢ ( ∀ 𝑤 𝑤 = 𝑠 → ∀ 𝑧 ∀ 𝑡 𝑢 = 𝑣 ) |
4 | 1 3 | syl | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 ∀ 𝑡 𝑢 = 𝑣 ) |