Theorem 19.23v 1972

Description: Version of 19.23 2247 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 1997. (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 1864	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1942	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 36	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1940	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 17	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1869	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 18	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 212	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  19.23vv  1973  pm11.53v  1974  equsv  2033  sb4b  2507  2mo2  2675  ceqsalv  3494  clel2g  3618  clel4g  3622  elabd2  3629  elabgt  3631  elabgtOLD  3632  euind  3687  reuind  3716  sbcg  3816  ralsng  4641  snssb  4748  unissb  4906  disjor  5091  dftr2  5220  ssrelrel  5782  cotrg  6111  fununi  6611  dff13  7252  dffi2  9379  aceq2  10099  psgnunilem4  19562  metcld  25465  metcld2  25466  isch2  31575  disjorf  32924  funcnv5mpt  33012  bnj1052  35363  bnj1030  35375  dfon2lem8  36280  mh-unprimbi  37055  mh-infprim1bi  37057  bj-ssbeq  37275  bj-ssbid2ALT  37285  bj-sblem1  37477  bj-sblem2  37478  bj-sblem  37479  wl-equsalvw  38193  ineleq  39003  cocossss  39175  cossssid3  39208  trcoss2  39223  elmapintrab  44302  elinintrab  44303  undmrnresiss  44330  elintima  44379  relexp0eq  44427  dfhe3  44501  ismnuprim  45004  pm10.52  45075  truniALT  45250  tpid3gVD  45550  truniALTVD  45586  onfrALTVD  45599  unisnALT  45634