Theorem 19.23v 1946

Description: Version of 19.23 2205 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 1972. (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 1837	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1916	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1914	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1842	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 208	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

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

This theorem is referenced by:  19.23vv  1947  pm11.53v  1948  equsv  2007  sb4b  2475  2mo2  2644  ceqsalv  3512  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  7254  dffi2  9418  aceq2  10114  psgnunilem4  19365  metcld  24823  metcld2  24824  isch2  30507  disjorf  31841  funcnv5mpt  31924  bnj1052  34017  bnj1030  34029  dfon2lem8  34793  bj-ssbeq  35578  bj-ssbid2ALT  35588  bj-sblem1  35769  bj-sblem2  35770  bj-sblem  35771  wl-equsalvw  36455  ineleq  37271  cocossss  37354  cossssid3  37387  trcoss2  37402  elmapintrab  42375  elinintrab  42376  undmrnresiss  42403  elintima  42452  relexp0eq  42500  dfhe3  42574  ismnuprim  43101  pm10.52  43172  truniALT  43350  tpid3gVD  43651  truniALTVD  43687  onfrALTVD  43700  unisnALT  43735