Theorem r19.23v 3180

Description: Restricted quantifier version of 19.23v 1943. Version of r19.23 3251 with a disjoint variable condition. (Contributed by NM, 31-Aug-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)

Assertion

Ref	Expression
r19.23v	⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem r19.23v

Step	Hyp	Ref	Expression
1		con34b 315	. . 3 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
2	1	ralbii 3091	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑))
3		r19.21v 3177	. 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
4		dfrex2 3071	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
5	4	imbi1i 348	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 → 𝜓) ↔ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓))
6		con1b 357	. . 3 ⊢ ((¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
7	5, 6	bitr2i 275	. 2 ⊢ ((¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
8	2, 3, 7	3bitri 296	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wral 3059  ∃wrex 3068

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-an 395  df-ex 1780  df-ral 3060  df-rex 3069

This theorem is referenced by:  rexlimivOLD  3182  ceqsralv  3512  ralxpxfr2d  3633  uniiunlem  4083  2reu4lem  4524  dfiin2g  5034  iunss  5047  ralxfr2d  5407  ssrel2  5784  reliun  5815  idrefALT  6111  dfpo2  6294  funimass4  6955  fnssintima  7361  ralrnmpo  7549  imaeqalov  7648  ttrclss  9717  kmlem12  10158  fimaxre3  12164  gcdcllem1  16444  vdwmc2  16916  iunocv  21453  islindf4  21612  ovolgelb  25229  dyadmax  25347  itg2leub  25484  eqscut2  27544  addsprop  27698  addsuniflem  27723  negsprop  27748  mulsprop  27825  mulsuniflem  27843  mptelee  28420  nmoubi  30292  nmopub  31428  nmfnleub  31445  sigaclcu2  33416  untuni  34982  elintfv  35040  heibor1lem  36980  ispsubsp2  38920  pmapglbx  38943  neik0pk1imk0  43100  2reuimp0  46120