Theorem 19.21v 1853

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 1506. 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 2011 derived from df-eu 2009. 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 1506	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2	1	19.21h 1537	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm11.53  1875  cbval2  1901  sbhb  1920  2sb6  1964  sbcom2v  1965  2sb6rf  1970  2exsb  1989  moanim  2080  r3al  2501  ceqsralt  2739  rspc2gv  2828  euind  2899  reu2  2900  reuind  2917  unissb  3804  dfiin2g  3884  tfi  4543  asymref  4973  dff13  5720  mpo2eqb  5932