Theorem r19.23v 3182

Description: Restricted quantifier version of 19.23v 1941. Version of r19.23 3255 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 316	. . 3 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
2	1	ralbii 3092	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑))
3		r19.21v 3179	. 2 ⊢ (∀𝑥 ∈ 𝐴 (¬ 𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
4		dfrex2 3072	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
5	4	imbi1i 349	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 → 𝜓) ↔ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓))
6		con1b 358	. . 3 ⊢ ((¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
7	5, 6	bitr2i 276	. 2 ⊢ ((¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
8	2, 3, 7	3bitri 297	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wral 3060  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-ral 3061  df-rex 3070

This theorem is referenced by:  rexlimivOLD  3184  ceqsralv  3521  ralxpxfr2d  3645  uniiunlem  4086  2reu4lem  4521  dfiin2g  5031  iunss  5044  ralxfr2d  5409  ssrel2  5794  reliun  5825  idrefALT  6130  dfpo2  6315  funimass4  6972  fnssintima  7383  ralrnmpo  7573  imaeqalov  7673  ttrclss  9761  kmlem12  10203  fimaxre3  12215  gcdcllem1  16537  vdwmc2  17018  iunocv  21700  islindf4  21859  ovolgelb  25516  dyadmax  25634  itg2leub  25770  eqscut2  27852  addsprop  28010  addsuniflem  28035  negsprop  28068  mulsprop  28157  mulsuniflem  28176  mptelee  28911  nmoubi  30792  nmopub  31928  nmfnleub  31945  sigaclcu2  34122  untuni  35710  elintfv  35766  heibor1lem  37817  ispsubsp2  39749  pmapglbx  39772  neik0pk1imk0  44065  2reuimp0  47131