Theorem r19.23v 3190

Description: Restricted quantifier version of 19.23v 1975. Version of r19.23 3260 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 3109	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑))
3		r19.21v 3188	. 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
4		dfrex2 3090	. . . 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 3077  ∃wrex 3087

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 3078  df-rex 3088

This theorem is used by:  ceqsralv  3491  ralxpxfr2d  3600  uniiunlem  4035  2reu4lem  4479  dfiin2g  4989  iunss  5003  iunssOLD  5004  replem  5241  ralxfr2d  5372  ssrel2  5761  idrefALT  6107  dfpo2  6298  funimass4  6947  fnssintima  7370  ralrnmpo  7557  imaeqalov  7658  ttrclss  9714  kmlem12  10233  fimaxre3  12256  gcdcllem1  16662  vdwmc2  17150  iunocv  21980  islindf4  22137  ovolgelb  25794  dyadmax  25912  itg2leub  26048  eqcuts2  28165  addsprop  28355  addsuniflem  28380  negsprop  28414  mulsprop  28509  mulsuniflem  28528  mpteleeOLD  29466  nmoubi  31367  nmopub  32503  nmfnleub  32520  sigaclcu2  34745  untuni  36453  elintfv  36509  heibor1lem  38723  ispsubsp2  40783  pmapglbx  40806  neik0pk1imk0  45032  2reuimp0  48153