Theorem 19.23v 1942

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  19.23vv  1943  pm11.53v  1944  equsv  2003  sb4b  2473  2mo2  2640  ceqsalv  3484  clel2g  3622  clel4g  3626  elabd2  3633  elabgt  3635  elabgtOLD  3636  elabgtOLDOLD  3637  euind  3692  reuind  3721  sbcg  3823  ralsng  4635  snssb  4742  unissb  4899  unissbOLD  4900  disjor  5084  dftr2  5211  ssrelrel  5750  cotrg  6069  cotrgOLD  6070  fununi  6575  dff13  7211  dffi2  9350  aceq2  10048  psgnunilem4  19403  metcld  25182  metcld2  25183  isch2  31125  disjorf  32481  funcnv5mpt  32565  bnj1052  34938  bnj1030  34950  dfon2lem8  35751  bj-ssbeq  36614  bj-ssbid2ALT  36624  bj-sblem1  36803  bj-sblem2  36804  bj-sblem  36805  wl-equsalvw  37499  ineleq  38309  cocossss  38400  cossssid3  38433  trcoss2  38448  elmapintrab  43538  elinintrab  43539  undmrnresiss  43566  elintima  43615  relexp0eq  43663  dfhe3  43737  ismnuprim  44256  pm10.52  44327  truniALT  44504  tpid3gVD  44804  truniALTVD  44840  onfrALTVD  44853  unisnALT  44888