Theorem 19.23v 1943

Description: Version of 19.23 2214 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 1968. (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 1835	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1913	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1911	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1840	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  19.23vv  1944  pm11.53v  1945  equsv  2004  sb4b  2475  2mo2  2642  ceqsalv  3476  clel2g  3609  clel4g  3613  elabd2  3620  elabgt  3622  elabgtOLD  3623  elabgtOLDOLD  3624  euind  3678  reuind  3707  sbcg  3809  ralsng  4623  snssb  4730  unissb  4886  disjor  5068  dftr2  5195  ssrelrel  5731  cotrg  6053  fununi  6551  dff13  7183  dffi2  9302  aceq2  10005  psgnunilem4  19404  metcld  25228  metcld2  25229  isch2  31195  disjorf  32551  funcnv5mpt  32642  bnj1052  34979  bnj1030  34991  dfon2lem8  35824  bj-ssbeq  36687  bj-ssbid2ALT  36697  bj-sblem1  36876  bj-sblem2  36877  bj-sblem  36878  wl-equsalvw  37572  ineleq  38382  cocossss  38473  cossssid3  38506  trcoss2  38521  elmapintrab  43609  elinintrab  43610  undmrnresiss  43637  elintima  43686  relexp0eq  43734  dfhe3  43808  ismnuprim  44327  pm10.52  44398  truniALT  44574  tpid3gVD  44874  truniALTVD  44910  onfrALTVD  44923  unisnALT  44958