Theorem aev2 2093

Description: A version of aev 2092 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 2091, aev 2092, aev2 2093).

Using aev 2092 and alrimiv 1960, 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 30848. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1828, ax-1 6-- ax-13 2407 (as the one-element universe shows), so for instance (∀𝑥𝑥 = 𝑦 → ⊥), DV (𝑥, 𝑦) is not provable from these axioms alone (indeed, dtru 5423 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 2092	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑤 𝑤 = 𝑠)
2		aev 2092	. . 3 ⊢ (∀𝑤 𝑤 = 𝑠 → ∀𝑡 𝑢 = 𝑣)
3	2	alrimiv 1960	. 2 ⊢ (∀𝑤 𝑤 = 𝑠 → ∀𝑧∀𝑡 𝑢 = 𝑣)
4	1, 3	syl 18	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  hbaev  2094