Theorem aev2 2095

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

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

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

This theorem is used by:  hbaev  2096