Theorem 19.23v 1943

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  ∃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 1911

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

This theorem is referenced by:  19.23vv  1944  pm11.53v  1945  equsv  2004  sb4b  2472  2mo2  2641  ceqsalv  3510  clel2g  3648  clel4g  3653  elabd2  3661  elabgt  3663  elabg  3667  euind  3721  reuind  3750  sbcg  3857  ralsng  4678  snssb  4787  unissb  4944  unissbOLD  4945  disjor  5129  dftr2  5268  ssrelrel  5797  cotrg  6109  cotrgOLD  6110  cotrgOLDOLD  6111  dffun2OLDOLD  6556  fununi  6624  dff13  7258  dffi2  9422  aceq2  10118  psgnunilem4  19408  metcld  25056  metcld2  25057  isch2  30741  disjorf  32075  funcnv5mpt  32158  bnj1052  34282  bnj1030  34294  dfon2lem8  35064  bj-ssbeq  35835  bj-ssbid2ALT  35845  bj-sblem1  36026  bj-sblem2  36027  bj-sblem  36028  wl-equsalvw  36712  ineleq  37528  cocossss  37611  cossssid3  37644  trcoss2  37659  elmapintrab  42631  elinintrab  42632  undmrnresiss  42659  elintima  42708  relexp0eq  42756  dfhe3  42830  ismnuprim  43357  pm10.52  43428  truniALT  43606  tpid3gVD  43907  truniALTVD  43943  onfrALTVD  43956  unisnALT  43991