Theorem 19.21v 1974

Description: Version of 19.21 2247 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 1974 versus 19.21 2247 and vtoclf 3529 versus vtocl 3524. 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 1949. 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 1973	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1947	. . . 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 1945

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

This theorem is used by:  19.32v  1975  pm11.53v  1979  19.12vvv  2029  cbvaldvaw  2073  2sb6  2125  sbrimvwOLD  2131  sbal  2209  sbrim  2341  pm11.53  2379  19.12vv  2380  sbhb  2553  r2al  3202  r3al  3204  ralcom4  3292  ceqsralt  3488  rspc2gv  3589  elabgtOLD  3630  euind  3685  reu2  3686  reuind  3714  sbccomlem  3821  unissb  4906  dfiin2g  4994  axrep5  5245  asymref  6128  fvn0ssdmfun  7106  dff13  7289  mpo2eqb  7583  xpord3inddlem  8208  findcard3  9312  marypha1lem  9462  marypha2lem3  9466  aceq1  10235  kmlem15  10282  cotr2g  15172  bnj864  35663  bnj865  35664  bnj978  35690  bnj1176  35746  bnj1186  35748  dfon2lem8  36767  dffun10  36891  mh-unprimbi  37547  mpobi123f  39360  mptbi12f  39364  sn-axrep5v  43538  unielss  44481  elmapintrab  44838  undmrnresiss  44865  dfhe3  45036  dffrege115  45239  ntrneiiso  45352  ntrneikb  45355  pm10.541  45612  pm10.542  45613  19.21vv  45621  pm11.62  45639  2sbc6g  45660  2rexsb  48445