Theorem r19.23v 3189

Description: Restricted quantifier version of 19.23v 1962. Version of r19.23 3259 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 318	. . 3 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
2	1	ralbii 3108	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑))
3		r19.21v 3187	. 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
4		dfrex2 3089	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
5	4	imbi1i 351	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 → 𝜓) ↔ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓))
6		con1b 360	. . 3 ⊢ ((¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
7	5, 6	bitr2i 278	. 2 ⊢ ((¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
8	2, 3, 7	3bitri 299	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208  ∀wral 3076  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-ral 3077  df-rex 3087

This theorem is referenced by:  ceqsralv  3494  ralxpxfr2d  3605  uniiunlem  4040  2reu4lem  4477  dfiin2g  4988  iunss  5002  iunssOLD  5003  replem  5238  ralxfr2d  5367  ssrel2  5757  idrefALT  6100  dfpo2  6283  funimass4  6931  fnssintima  7346  ralrnmpo  7535  imaeqalov  7635  ttrclss  9675  kmlem12  10118  fimaxre3  12138  gcdcllem1  16533  vdwmc2  17015  iunocv  21730  islindf4  21887  ovolgelb  25539  dyadmax  25657  itg2leub  25793  eqcuts2  27876  addsprop  28066  addsuniflem  28091  negsprop  28125  mulsprop  28220  mulsuniflem  28239  mpteleeOLD  29093  nmoubi  30972  nmopub  32108  nmfnleub  32125  sigaclcu2  34414  untuni  36056  elintfv  36112  heibor1lem  38305  ispsubsp2  40367  pmapglbx  40390  neik0pk1imk0  44620  2reuimp0  47705