Theorem r19.23v 3198

Description: Restricted quantifier version of 19.23v 1969. Version of r19.23 3268 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 3117	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑))
3		r19.21v 3196	. 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
4		dfrex2 3098	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
5	4	imbi1i 352	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 → 𝜓) ↔ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓))
6		con1b 361	. . 3 ⊢ ((¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
7	5, 6	bitr2i 279	. 2 ⊢ ((¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
8	2, 3, 7	3bitri 300	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wral 3085  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-ral 3086  df-rex 3096

This theorem is referenced by:  ceqsralv  3503  ralxpxfr2d  3614  uniiunlem  4049  2reu4lem  4489  dfiin2g  4999  iunss  5013  iunssOLD  5014  replem  5253  ralxfr2d  5382  ssrel2  5772  idrefALT  6114  dfpo2  6298  funimass4  6946  fnssintima  7361  ralrnmpo  7550  imaeqalov  7650  ttrclss  9688  kmlem12  10144  fimaxre3  12160  gcdcllem1  16556  vdwmc2  17038  iunocv  21799  islindf4  21956  ovolgelb  25607  dyadmax  25725  itg2leub  25861  eqcuts2  27944  addsprop  28134  addsuniflem  28159  negsprop  28193  mulsprop  28288  mulsuniflem  28307  mpteleeOLD  29185  nmoubi  31064  nmopub  32200  nmfnleub  32217  sigaclcu2  34454  untuni  36099  elintfv  36155  heibor1lem  38347  ispsubsp2  40409  pmapglbx  40432  neik0pk1imk0  44664  2reuimp0  47739