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 3173
Description: Restricted quantifier version of 19.23v 1938. Version of r19.23 3244 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
StepHypRef Expression
1 con34b 315 . . 3 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
21ralbii 3083 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴𝜓 → ¬ 𝜑))
3 r19.21v 3170 . 2 (∀𝑥𝐴𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
4 dfrex2 3063 . . . 4 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
54imbi1i 348 . . 3 ((∃𝑥𝐴 𝜑𝜓) ↔ (¬ ∀𝑥𝐴 ¬ 𝜑𝜓))
6 con1b 357 . . 3 ((¬ ∀𝑥𝐴 ¬ 𝜑𝜓) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
75, 6bitr2i 275 . 2 ((¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑) ↔ (∃𝑥𝐴 𝜑𝜓))
82, 3, 73bitri 296 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wral 3051  wrex 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-ral 3052  df-rex 3061
This theorem is referenced by:  rexlimivOLD  3175  ceqsralv  3504  ralxpxfr2d  3631  uniiunlem  4083  2reu4lem  4530  dfiin2g  5042  iunss  5055  ralxfr2d  5416  ssrel2  5793  reliun  5824  idrefALT  6125  dfpo2  6309  funimass4  6969  fnssintima  7376  ralrnmpo  7567  imaeqalov  7667  ttrclss  9765  kmlem12  10206  fimaxre3  12214  gcdcllem1  16501  vdwmc2  16983  iunocv  21679  islindf4  21838  ovolgelb  25503  dyadmax  25621  itg2leub  25758  eqscut2  27839  addsprop  27993  addsuniflem  28018  negsprop  28047  mulsprop  28134  mulsuniflem  28153  mptelee  28832  nmoubi  30708  nmopub  31844  nmfnleub  31861  sigaclcu2  33955  untuni  35533  elintfv  35590  heibor1lem  37512  ispsubsp2  39447  pmapglbx  39470  neik0pk1imk0  43732  2reuimp0  46745
  Copyright terms: Public domain W3C validator