Theorem aev2 2056

Description: A version of aev 2055 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 2054, aev 2055, aev2 2056).

Using aev 2055 and alrimiv 1925, 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 30489. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1792, ax-1 6-- ax-13 2375 (as the one-element universe shows), so for instance (∀𝑥𝑥 = 𝑦 → ⊥), DV (𝑥, 𝑦) is not provable from these axioms alone (indeed, dtru 5447 uses non-logical axioms as well). (Contributed by BJ, 23-Mar-2021.)

Assertion

Ref	Expression
aev2	⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣)

Distinct variable group:   𝑥,𝑦

Proof of Theorem aev2

Dummy variables 𝑤 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		aev 2055	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑤 𝑤 = 𝑠)
2		aev 2055	. . 3 ⊢ (∀𝑤 𝑤 = 𝑠 → ∀𝑡 𝑢 = 𝑣)
3	2	alrimiv 1925	. 2 ⊢ (∀𝑤 𝑤 = 𝑠 → ∀𝑧∀𝑡 𝑢 = 𝑣)
4	1, 3	syl 17	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣)

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777

This theorem is referenced by:  hbaev  2057