Theorem 19.23v 1946

Description: Version of 19.23 2207 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 1537  ∃wex 1783

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

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

This theorem is referenced by:  19.23vv  1947  pm11.53v  1948  equsv  2007  sbequ2OLD  2245  sb4b  2475  sb4bOLD  2476  2mo2  2649  ceqsalv  3457  clel2g  3581  clel4g  3586  elabd2  3594  elabgt  3596  elabg  3600  euind  3654  reuind  3683  sbcg  3791  ralsng  4606  unissb  4870  disjor  5050  dftr2  5189  ssrelrel  5695  cotrg  6005  dffun2  6428  fununi  6493  dff13  7109  dffi2  9112  aceq2  9806  psgnunilem4  19020  metcld  24375  metcld2  24376  isch2  29486  disjorf  30819  funcnv5mpt  30907  bnj1052  32855  bnj1030  32867  dfon2lem8  33672  bj-ssbeq  34761  bj-ssbid2ALT  34771  bj-sblem1  34953  bj-sblem2  34954  bj-sblem  34955  wl-equsalvw  35624  ineleq  36413  cocossss  36486  cossssid3  36514  trcoss2  36529  elmapintrab  41073  elinintrab  41074  undmrnresiss  41101  elintima  41150  relexp0eq  41198  dfhe3  41272  ismnuprim  41801  pm10.52  41872  truniALT  42050  tpid3gVD  42351  truniALTVD  42387  onfrALTVD  42400  unisnALT  42435