Theorem 19.23v 1944

Description: Version of 19.23 2219 with a disjoint variable condition instead of a nonfreeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.) Remove dependency on ax-6 1969. (Revised by Rohan Ridenour, 15-Apr-2022.)

Assertion

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

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.23v

Step	Hyp	Ref	Expression
1		exim 1836	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1914	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1912	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1841	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  19.23vv  1945  pm11.53v  1946  equsv  2005  sb4b  2480  2mo2  2648  ceqsalv  3482  clel2g  3615  clel4g  3619  elabd2  3626  elabgt  3628  elabgtOLD  3629  elabgtOLDOLD  3630  euind  3684  reuind  3713  sbcg  3815  ralsng  4634  snssb  4741  unissb  4898  disjor  5082  dftr2  5209  ssrelrel  5753  cotrg  6076  fununi  6575  dff13  7210  dffi2  9338  aceq2  10041  psgnunilem4  19438  metcld  25274  metcld2  25275  isch2  31311  disjorf  32666  funcnv5mpt  32757  bnj1052  35151  bnj1030  35163  dfon2lem8  36004  bj-ssbeq  36898  bj-ssbid2ALT  36908  bj-sblem1  37090  bj-sblem2  37091  bj-sblem  37092  wl-equsalvw  37793  ineleq  38605  cocossss  38777  cossssid3  38810  trcoss2  38825  elmapintrab  43932  elinintrab  43933  undmrnresiss  43960  elintima  44009  relexp0eq  44057  dfhe3  44131  ismnuprim  44650  pm10.52  44721  truniALT  44897  tpid3gVD  45197  truniALTVD  45233  onfrALTVD  45246  unisnALT  45281