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 3157
Description: Restricted quantifier version of 19.23v 2016. Version of r19.23 3156 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 305 . . 3 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
21ralbii 3114 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴𝜓 → ¬ 𝜑))
3 r19.21v 3094 . 2 (∀𝑥𝐴𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
4 dfrex2 3130 . . . 4 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
54imbi1i 338 . . 3 ((∃𝑥𝐴 𝜑𝜓) ↔ (¬ ∀𝑥𝐴 ¬ 𝜑𝜓))
6 con1b 347 . . 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 3046  wrex 3047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1850  df-ral 3051  df-rex 3052
This theorem is referenced by:  rexlimiv  3161  ralxpxfr2d  3462  uniiunlem  3829  dfiin2g  4701  iunss  4709  ralxfr2d  5027  ssrel2  5363  reliun  5391  funimass4  6405  ralrnmpt2  6936  kmlem12  9171  fimaxre3  11158  gcdcllem1  15419  vdwmc2  15881  iunocv  20223  islindf4  20375  ovolgelb  23444  dyadmax  23562  itg2leub  23696  mptelee  25970  nmoubi  27932  nmopub  29072  nmfnleub  29089  sigaclcu2  30488  untuni  31889  dfpo2  31948  elintfv  31965  heibor1lem  33917  ispsubsp2  35531  pmapglbx  35554  neik0pk1imk0  38843  2reu4a  41691
  Copyright terms: Public domain W3C validator