| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Axiom of Specialization.
A quantified wff implies the wff without a
quantifier (i.e. an instance, or special case, of the generalized wff).
In other words if something is true for all Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1593. Conditional forms of the converse are given by ax-12 1598, ax-15 2015, ax-16 1854, and ax-17 1605.
Unlike the more general textbook Axiom of Specialization, we cannot choose
a variable different from An nice alternate axiomatization uses ax467 1659 and ax-5o 1610 in place of ax-4 1608, ax-5 1590, ax-6 1591, and ax-7 1592. This axiom is redundant in the presence of certain other axioms, as shown by theorem ax4 1607. (We replaced the older ax-5o 1610 and ax-6o 1613 with newer versions ax-5 1590 and ax-6 1591 in order to prove this redundancy.) |
| Ref | Expression |
|---|---|
| ax-4 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph |
. . 3
| |
| 2 | vx |
. . 3
| |
| 3 | 1, 2 | wal 1584 |
. 2
|
| 4 | 3, 1 | wi 3 |
1
|
| Colors of variables: wff set class |
| This axiom is referenced by: ax5o 1609 ax5 1611 ax6o 1612 ax6 1614 a4i 1617 a4s 1619 a4sd 1620 ax46 1653 ax67to6 1657 ax467 1659 19.8a 1665 19.3 1667 19.12 1683 19.21 1692 19.21bi 1696 19.38 1718 19.21t 1755 19.23t 1756 hbae 1786 equs4 1791 equveli 1812 sb2 1821 ax11 1865 ax11b 1866 dfsb2 1871 sbf3t 1894 hbsb4 1895 hbsb4t 1896 sb56 1913 sb6 1914 a16gb 1924 sbal1 2001 ax11indalem 2023 ax11inda2ALT 2024 mopick 2094 2eu1 2112 ra4 2406 ralcom2 2490 ceqex 2631 vtoclgft 2671 hbsbcgd 2750 intab 3428 axrep1 3597 axrep2 3598 axnulALT 3611 dtru 3662 copsex2t 3701 ssopab2 3734 eusv1 3960 eusv2OLD 3963 eusv2 3964 alxfr 3982 fununi 4582 hbfvd2 4773 dffv2 4820 fiint 5872 nd3 6459 axrepndlem2 6463 axrepnd 6464 axpowndlem2 6468 axpowndlem4 6470 axinfndlem1 6475 axacndlem4 6480 axacndlem5 6481 suppsrlem 6739 cncnplem2 9918 inficlALT 11047 bnj32 13195 bnj954 13621 bnj569 14058 bnj1073 14174 tz6.26 14558 frmin 14591 wfrlem5 14614 frrlem5 14638 imonclem 15956 inficlALTOLD 16196 prtlem14 17101 pm11.57 17170 pm11.59 17172 ax4567to6 17186 ax4567to7 17187 ax10ext 17188 ax10-16 17189 pm14.123b 17214 eubi 17226 compne 17241 |