Theorem 19.23v 1940

Description: Version of 19.23 2209 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 1965. (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 1831	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1910	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1908	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1836	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

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

This theorem is referenced by:  19.23vv  1941  pm11.53v  1942  equsv  2000  sb4b  2478  2mo2  2645  ceqsalv  3519  clel2g  3659  clel4g  3663  elabd2  3670  elabgt  3672  elabgtOLD  3673  elabg  3677  euind  3733  reuind  3762  sbcg  3870  ralsng  4680  snssb  4787  unissb  4944  unissbOLD  4945  disjor  5130  dftr2  5267  ssrelrel  5809  cotrg  6130  cotrgOLD  6131  cotrgOLDOLD  6132  dffun2OLDOLD  6575  fununi  6643  dff13  7275  dffi2  9461  aceq2  10157  psgnunilem4  19530  metcld  25354  metcld2  25355  isch2  31252  disjorf  32599  funcnv5mpt  32685  bnj1052  34968  bnj1030  34980  dfon2lem8  35772  bj-ssbeq  36636  bj-ssbid2ALT  36646  bj-sblem1  36825  bj-sblem2  36826  bj-sblem  36827  wl-equsalvw  37519  ineleq  38336  cocossss  38418  cossssid3  38451  trcoss2  38466  elmapintrab  43566  elinintrab  43567  undmrnresiss  43594  elintima  43643  relexp0eq  43691  dfhe3  43765  ismnuprim  44290  pm10.52  44361  truniALT  44539  tpid3gVD  44840  truniALTVD  44876  onfrALTVD  44889  unisnALT  44924