Theorem 19.21v 1972

Description: Version of 19.21 2246 with a disjoint variable condition, requiring fewer axioms.

Notational convention: We sometimes suffix with "v" the label of a theorem using a distinct variable ("dv") condition instead of a nonfreeness hypothesis such as Ⅎ𝑥𝜑. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a nonfreeness hypothesis ("f" stands for "not free in", see df-nf 1817) instead of a disjoint variable condition. For instance, 19.21v 1972 versus 19.21 2246 and vtoclf 3532 versus vtocl 3527. Note that "not free in" is less restrictive than "does not occur in". Note that the version with a disjoint variable condition is easily proved from the version with the corresponding nonfreeness hypothesis, by using nfv 1947. However, the dv version can often be proved from fewer axioms. (Contributed by NM, 21-Jun-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 12-Jul-2020.)

Assertion

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

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.21v

Step	Hyp	Ref	Expression
1		stdpc5v 1971	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1945	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 64	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1872	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 18	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 212	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  19.32v  1973  pm11.53v  1977  19.12vvv  2027  cbvaldvaw  2071  2sb6  2123  sbrimvwOLD  2129  sbal  2207  sbrim  2341  pm11.53  2380  19.12vv  2381  sbhb  2555  r2al  3203  r3al  3205  ralcom4  3293  ceqsralt  3491  rspc2gv  3593  elabgtOLD  3634  euind  3689  reu2  3690  reuind  3718  sbccomlem  3824  unissb  4908  dfiin2g  4997  axrep5  5248  asymref  6118  fvn0ssdmfun  7073  dff13  7257  mpo2eqb  7551  xpord3inddlem  8156  findcard3  9250  marypha1lem  9400  marypha2lem3  9404  aceq1  10117  kmlem15  10164  cotr2g  15037  bnj864  35375  bnj865  35376  bnj978  35402  bnj1176  35458  bnj1186  35460  dfon2lem8  36317  dffun10  36441  mh-unprimbi  37112  mpobi123f  38869  mptbi12f  38873  sn-axrep5v  43046  unielss  44003  elmapintrab  44360  undmrnresiss  44388  dfhe3  44559  dffrege115  44762  ntrneiiso  44875  ntrneikb  44878  pm10.541  45135  pm10.542  45136  19.21vv  45144  pm11.62  45162  2sbc6g  45183  2rexsb  47896