Theorem aev2 2092

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

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

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

This theorem is used by:  hbaev  2093