Theorem 19.21v 1846

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 1563 via the use of distinct variable conditions combined with ax-17 1507. 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 2005 derived from df-eu 2003. 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 1507	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2	1	19.21h 1537	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ial 1515  ax-i5r 1516

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm11.53  1868  cbval2  1894  sbhb  1914  2sb6  1960  sbcom2v  1961  2sb6rf  1966  2exsb  1985  moanim  2074  r3al  2480  ceqsralt  2716  rspc2gv  2805  euind  2875  reu2  2876  reuind  2893  unissb  3774  dfiin2g  3854  tfi  4504  asymref  4932  dff13  5677  mpo2eqb  5888