Theorem 19.21v 1897

Description: Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as (𝜑 → ∀𝑥𝜑) in 19.21 1607 via the use of distinct variable conditions combined with ax-17 1550. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g., euf 2060 derived from df-eu 2058. The "f" stands for "not free in" which is less restrictive than "does not occur in". (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
19.21v	⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.21v

Step	Hyp	Ref	Expression
1		ax-17 1550	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2	1	19.21h 1581	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm11.53  1920  cbval2  1946  cbvaldvaw  1955  sbhb  1969  2sb6  2013  sbcom2v  2014  2sb6rf  2019  2exsb  2038  moanim  2129  r3al  2551  ceqsralt  2801  rspc2gv  2893  euind  2964  reu2  2965  reuind  2982  unissb  3886  dfiin2g  3966  tfi  4638  asymref  5077  dff13  5850  mpo2eqb  6068