Theorem 19.23v 1974

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 1999. (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 1866	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1944	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 36	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1942	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 17	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1871	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 18	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 212	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  19.23vv  1975  pm11.53v  1976  equsv  2035  sb4b  2504  2mo2  2672  ceqsalv  3489  clel2g  3612  clel4g  3616  elabd2  3623  elabgt  3625  elabgtOLD  3626  euind  3681  reuind  3710  sbcg  3810  ralsng  4632  snssb  4739  unissb  4900  disjor  5084  dftr2  5213  ssrelrel  5773  cotrg  6107  fununi  6620  dff13  7262  dffi2  9422  aceq2  10205  psgnunilem4  19720  metcld  25636  metcld2  25637  isch2  31834  disjorf  33224  funcnv5mpt  33312  bnj1052  35655  bnj1030  35667  dfon2lem8  36648  mh-unprimbi  37428  mh-infprim1bi  37430  bj-ssbeq  37648  bj-ssbid2ALT  37658  bj-sblem1  37850  bj-sblem2  37851  bj-sblem  37852  wl-equsalvw  38579  ineleq  39395  cocossss  39567  cossssid3  39600  trcoss2  39615  elmapintrab  44686  elinintrab  44687  undmrnresiss  44713  elintima  44762  relexp0eq  44810  dfhe3  44884  ismnuprim  45387  pm10.52  45458  truniALT  45632  tpid3gVD  45932  truniALTVD  45968  onfrALTVD  45981  unisnALT  46016