MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  aev2 Structured version   Visualization version   GIF version

Theorem aev2 2058
Description: A version of aev 2057 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 2056, aev 2057, aev2 2058).

Using aev 2057 and alrimiv 1927, 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 30479. This list cannot be extended to ¬ or since the scheme 𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1795, ax-1 6-- ax-13 2377 (as the one-element universe shows), so for instance (∀𝑥𝑥 = 𝑦 → ⊥), DV (𝑥, 𝑦) is not provable from these axioms alone (indeed, dtru 5441 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.
StepHypRef Expression
1 aev 2057 . 2 (∀𝑥 𝑥 = 𝑦 → ∀𝑤 𝑤 = 𝑠)
2 aev 2057 . . 3 (∀𝑤 𝑤 = 𝑠 → ∀𝑡 𝑢 = 𝑣)
32alrimiv 1927 . 2 (∀𝑤 𝑤 = 𝑠 → ∀𝑧𝑡 𝑢 = 𝑣)
41, 3syl 17 1 (∀𝑥 𝑥 = 𝑦 → ∀𝑧𝑡 𝑢 = 𝑣)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780
This theorem is referenced by:  hbaev  2059
  Copyright terms: Public domain W3C validator