Theorem r19.23v 3194

Description: Restricted quantifier version of 19.23v 1975. Version of r19.23 3264 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 3113	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑))
3		r19.21v 3192	. 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
4		dfrex2 3094	. . . 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 3081  ∃wrex 3091

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 3082  df-rex 3092

This theorem is used by:  ceqsralv  3497  ralxpxfr2d  3607  uniiunlem  4042  2reu4lem  4486  dfiin2g  4997  iunss  5011  iunssOLD  5012  replem  5251  ralxfr2d  5383  ssrel2  5773  idrefALT  6115  dfpo2  6301  funimass4  6949  fnssintima  7371  ralrnmpo  7558  imaeqalov  7659  ttrclss  9696  kmlem12  10161  fimaxre3  12176  gcdcllem1  16579  vdwmc2  17061  iunocv  21881  islindf4  22038  ovolgelb  25690  dyadmax  25808  itg2leub  25944  eqcuts2  28030  addsprop  28220  addsuniflem  28245  negsprop  28279  mulsprop  28374  mulsuniflem  28393  mpteleeOLD  29300  nmoubi  31195  nmopub  32331  nmfnleub  32348  sigaclcu2  34574  untuni  36238  elintfv  36294  heibor1lem  38518  ispsubsp2  40578  pmapglbx  40601  neik0pk1imk0  44831  2reuimp0  47909