Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Axiom scheme ax-5 (Distinctness) - first use of $d
ax5ea
Metamath Proof Explorer
Description: If a formula holds for some value of a variable not occurring in it,
then it holds for all values of that variable. (Contributed by BJ , 28-Dec-2020)

Ref
Expression
Assertion
ax5ea
$${\u22a2}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi}$$

Proof
Step
Hyp
Ref
Expression
1
ax5e
$${\u22a2}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to {\phi}$$
2
ax-5
$${\u22a2}{\phi}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi}$$
3
1 2
syl
$${\u22a2}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi}$$