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  2479  2mo2  2647  ceqsalv  3469  clel2g  3601  clel4g  3605  elabd2  3612  elabgt  3614  elabgtOLD  3615  elabgtOLDOLD  3616  euind  3670  reuind  3699  sbcg  3801  ralsng  4619  snssb  4726  unissb  4883  disjor  5067  dftr2  5194  ssrelrel  5752  cotrg  6074  fununi  6573  dff13  7209  dffi2  9336  aceq2  10041  psgnunilem4  19472  metcld  25273  metcld2  25274  isch2  31294  disjorf  32649  funcnv5mpt  32740  bnj1052  35117  bnj1030  35129  dfon2lem8  35970  mh-unprimbi  36726  mh-infprim1bi  36728  bj-ssbeq  36947  bj-ssbid2ALT  36957  bj-sblem1  37149  bj-sblem2  37150  bj-sblem  37151  wl-equsalvw  37863  ineleq  38675  cocossss  38847  cossssid3  38880  trcoss2  38895  elmapintrab  44003  elinintrab  44004  undmrnresiss  44031  elintima  44080  relexp0eq  44128  dfhe3  44202  ismnuprim  44721  pm10.52  44792  truniALT  44968  tpid3gVD  45268  truniALTVD  45304  onfrALTVD  45317  unisnALT  45352