Theorem r19.23v 3189

Description: Restricted quantifier version of 19.23v 1974. 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 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  ceqsralv  3490  ralxpxfr2d  3599  uniiunlem  4011  2reu4lem  4478  dfiin2g  4988  iunss  5002  iunssOLD  5003  replem  5240  ralxfr2d  5372  ssrel2  5762  idrefALT  6109  dfpo2  6302  funimass4  6954  fnssintima  7376  ralrnmpo  7563  imaeqalov  7664  ovmptss  8108  ttrclss  9728  kmlem12  10247  fimaxre3  12270  gcdcllem1  16678  vdwmc2  17166  iunocv  21996  islindf4  22153  ovolgelb  25810  dyadmax  25928  itg2leub  26064  eqcuts2  28181  addsprop  28371  addsuniflem  28396  negsprop  28430  mulsprop  28525  mulsuniflem  28544  mpteleeOLD  29482  nmoubi  31383  nmopub  32519  nmfnleub  32536  sigaclcu2  34802  untuni  36570  elintfv  36626  heibor1lem  38852  ispsubsp2  40912  pmapglbx  40935  neik0pk1imk0  45156  2reuimp0  48293