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  3487  clel2g  3625  clel4g  3629  elabd2  3636  elabgt  3638  elabgtOLD  3639  elabgtOLDOLD  3640  euind  3695  reuind  3724  sbcg  3826  ralsng  4639  snssb  4746  unissb  4903  unissbOLD  4904  disjor  5089  dftr2  5216  ssrelrel  5759  cotrg  6080  cotrgOLD  6081  cotrgOLDOLD  6082  dffun2OLDOLD  6523  fununi  6591  dff13  7229  dffi2  9374  aceq2  10072  psgnunilem4  19427  metcld  25206  metcld2  25207  isch2  31152  disjorf  32508  funcnv5mpt  32592  bnj1052  34965  bnj1030  34977  dfon2lem8  35778  bj-ssbeq  36641  bj-ssbid2ALT  36651  bj-sblem1  36830  bj-sblem2  36831  bj-sblem  36832  wl-equsalvw  37526  ineleq  38336  cocossss  38427  cossssid3  38460  trcoss2  38475  elmapintrab  43565  elinintrab  43566  undmrnresiss  43593  elintima  43642  relexp0eq  43690  dfhe3  43764  ismnuprim  44283  pm10.52  44354  truniALT  44531  tpid3gVD  44831  truniALTVD  44867  onfrALTVD  44880  unisnALT  44915