Theorem 19.21v 1972

Description: Version of 19.21 2244 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 2244 and vtoclf 3526 versus vtocl 3521. 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  2206  sbrim  2338  pm11.53  2376  19.12vv  2377  sbhb  2551  r2al  3199  r3al  3201  ralcom4  3289  ceqsralt  3485  rspc2gv  3586  elabgtOLD  3627  euind  3682  reu2  3683  reuind  3711  sbccomlem  3817  unissb  4901  dfiin2g  4989  axrep5  5239  asymref  6110  fvn0ssdmfun  7072  dff13  7256  mpo2eqb  7550  xpord3inddlem  8164  findcard3  9267  marypha1lem  9418  marypha2lem3  9422  aceq1  10189  kmlem15  10236  cotr2g  15122  bnj864  35545  bnj865  35546  bnj978  35572  bnj1176  35628  bnj1186  35630  dfon2lem8  36532  dffun10  36656  mh-unprimbi  37312  mpobi123f  39074  mptbi12f  39078  sn-axrep5v  43251  unielss  44204  elmapintrab  44561  undmrnresiss  44589  dfhe3  44760  dffrege115  44963  ntrneiiso  45076  ntrneikb  45079  pm10.541  45336  pm10.542  45337  19.21vv  45345  pm11.62  45363  2sbc6g  45384  2rexsb  48140