![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > ax-12 | Unicode version |
Description: Axiom of Quantified
Equality. One of the equality and substitution axioms
of predicate calculus with equality.
An equivalent way to express this axiom that may be easier to understand
is The original version of this axiom was ax-12o 2142 and was replaced with this shorter ax-12 1925 in December 2015. The old axiom is proved from this one as Theorem ax12o 1934. Conversely, this axiom is proved from ax-12o 2142 as Theorem ax12 1935.
The primary purpose of this axiom is to provide a way to introduce the
quantifier
Although this version is shorter, the original version ax12o 1934 may be more
practical to work with because of the "distinctor" form of its
antecedents. A typical application of ax12o 1934 is in dvelimh 1964 which
converts a distinct variable pair to the distinctor antecendent
This axiom can be weakened if desired by adding distinct variable
restrictions on pairs This axiom scheme is logically redundant (see ax12w 1724) but is used as an auxiliary axiom to achieve metalogical completeness. (Contributed by NM, 21-Dec-2015.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax-12 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx |
. . . 4
![]() ![]() | |
2 | vy |
. . . 4
![]() ![]() | |
3 | 1, 2 | weq 1643 |
. . 3
![]() ![]() ![]() ![]() |
4 | 3 | wn 3 |
. 2
![]() ![]() ![]() ![]() ![]() |
5 | vz |
. . . 4
![]() ![]() | |
6 | 2, 5 | weq 1643 |
. . 3
![]() ![]() ![]() ![]() |
7 | 6, 1 | wal 1540 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
8 | 6, 7 | wi 4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wi 4 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This axiom is referenced by: ax12v 1926 |
Copyright terms: Public domain | W3C validator |