Theorem r19.23v 3189

Description: Restricted quantifier version of 19.23v 1975. 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 319	. . 3 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
2	1	ralbii 3108	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑))
3		r19.21v 3187	. 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
4		dfrex2 3089	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
5	4	imbi1i 352	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 → 𝜓) ↔ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓))
6		con1b 361	. . 3 ⊢ ((¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
7	5, 6	bitr2i 279	. 2 ⊢ ((¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
8	2, 3, 7	3bitri 300	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wral 3076  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3077  df-rex 3087

This theorem is used by:  ceqsralv  3490  ralxpxfr2d  3600  uniiunlem  4035  2reu4lem  4479  dfiin2g  4989  iunss  5003  iunssOLD  5004  replem  5243  ralxfr2d  5375  ssrel2  5765  idrefALT  6107  dfpo2  6294  funimass4  6942  fnssintima  7365  ralrnmpo  7552  imaeqalov  7653  ttrclss  9699  kmlem12  10164  fimaxre3  12185  gcdcllem1  16589  vdwmc2  17071  iunocv  21894  islindf4  22051  ovolgelb  25708  dyadmax  25826  itg2leub  25962  eqcuts2  28051  addsprop  28241  addsuniflem  28266  negsprop  28300  mulsprop  28395  mulsuniflem  28414  mpteleeOLD  29352  nmoubi  31253  nmopub  32389  nmfnleub  32406  sigaclcu2  34630  untuni  36288  elintfv  36344  heibor1lem  38559  ispsubsp2  40619  pmapglbx  40642  neik0pk1imk0  44887  2reuimp0  48002