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  3470  clel2g  3602  clel4g  3606  elabd2  3613  elabgt  3615  elabgtOLD  3616  elabgtOLDOLD  3617  euind  3671  reuind  3700  sbcg  3802  ralsng  4620  snssb  4727  unissb  4884  disjor  5068  dftr2  5195  ssrelrel  5743  cotrg  6066  fununi  6565  dff13  7200  dffi2  9327  aceq2  10030  psgnunilem4  19430  metcld  25251  metcld2  25252  isch2  31283  disjorf  32638  funcnv5mpt  32729  bnj1052  35123  bnj1030  35135  dfon2lem8  35976  bj-ssbeq  36945  bj-ssbid2ALT  36955  bj-sblem1  37147  bj-sblem2  37148  bj-sblem  37149  wl-equsalvw  37854  ineleq  38666  cocossss  38838  cossssid3  38871  trcoss2  38886  elmapintrab  44006  elinintrab  44007  undmrnresiss  44034  elintima  44083  relexp0eq  44131  dfhe3  44205  ismnuprim  44724  pm10.52  44795  truniALT  44971  tpid3gVD  45271  truniALTVD  45307  onfrALTVD  45320  unisnALT  45355