Theorem 19.23v 1941

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 1832	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1911	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1909	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1837	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-ex 1778

This theorem is referenced by:  19.23vv  1942  pm11.53v  1943  equsv  2002  sb4b  2483  2mo2  2650  ceqsalv  3529  clel2g  3672  clel4g  3676  elabd2  3683  elabgt  3685  elabgtOLD  3686  elabg  3690  euind  3746  reuind  3775  sbcg  3883  ralsng  4697  snssb  4807  unissb  4963  unissbOLD  4964  disjor  5148  dftr2  5285  ssrelrel  5820  cotrg  6139  cotrgOLD  6140  cotrgOLDOLD  6141  dffun2OLDOLD  6585  fununi  6653  dff13  7292  dffi2  9492  aceq2  10188  psgnunilem4  19539  metcld  25359  metcld2  25360  isch2  31255  disjorf  32601  funcnv5mpt  32686  bnj1052  34951  bnj1030  34963  dfon2lem8  35754  bj-ssbeq  36619  bj-ssbid2ALT  36629  bj-sblem1  36808  bj-sblem2  36809  bj-sblem  36810  wl-equsalvw  37492  ineleq  38310  cocossss  38392  cossssid3  38425  trcoss2  38440  elmapintrab  43538  elinintrab  43539  undmrnresiss  43566  elintima  43615  relexp0eq  43663  dfhe3  43737  ismnuprim  44263  pm10.52  44334  truniALT  44512  tpid3gVD  44813  truniALTVD  44849  onfrALTVD  44862  unisnALT  44897