MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.23v Structured version   Visualization version   GIF version

Theorem r19.23v 3017
Description: Restricted quantifier version of 19.23v 1899. Version of r19.23 3016 with a dv 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
StepHypRef Expression
1 con34b 306 . . 3 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
21ralbii 2975 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴𝜓 → ¬ 𝜑))
3 r19.21v 2955 . 2 (∀𝑥𝐴𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
4 dfrex2 2991 . . . 4 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
54imbi1i 339 . . 3 ((∃𝑥𝐴 𝜑𝜓) ↔ (¬ ∀𝑥𝐴 ¬ 𝜑𝜓))
6 con1b 348 . . 3 ((¬ ∀𝑥𝐴 ¬ 𝜑𝜓) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
75, 6bitr2i 265 . 2 ((¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑) ↔ (∃𝑥𝐴 𝜑𝜓))
82, 3, 73bitri 286 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wral 2907  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2912  df-rex 2913
This theorem is referenced by:  rexlimiv  3021  ralxpxfr2d  3315  uniiunlem  3674  dfiin2g  4524  iunss  4532  ralxfr2d  4847  ssrel2  5176  reliun  5205  funimass4  6209  ralrnmpt2  6735  kmlem12  8935  fimaxre3  10922  gcdcllem1  15156  vdwmc2  15618  iunocv  19957  islindf4  20109  ovolgelb  23171  dyadmax  23289  itg2leub  23424  mptelee  25692  nmoubi  27497  nmopub  28637  nmfnleub  28654  sigaclcu2  29988  untuni  31329  dfpo2  31388  heibor1lem  33275  ispsubsp2  34547  pmapglbx  34570  neik0pk1imk0  37862  2reu4a  40519
  Copyright terms: Public domain W3C validator