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 3183
Description: Restricted quantifier version of 19.23v 1946. Version of r19.23 3254 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 316 . . 3 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
21ralbii 3094 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴𝜓 → ¬ 𝜑))
3 r19.21v 3180 . 2 (∀𝑥𝐴𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
4 dfrex2 3074 . . . 4 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
54imbi1i 350 . . 3 ((∃𝑥𝐴 𝜑𝜓) ↔ (¬ ∀𝑥𝐴 ¬ 𝜑𝜓))
6 con1b 359 . . 3 ((¬ ∀𝑥𝐴 ¬ 𝜑𝜓) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
75, 6bitr2i 276 . 2 ((¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑) ↔ (∃𝑥𝐴 𝜑𝜓))
82, 3, 73bitri 297 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wral 3062  wrex 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063  df-rex 3072
This theorem is referenced by:  rexlimivOLD  3185  ceqsralv  3514  ralxpxfr2d  3635  uniiunlem  4085  2reu4lem  4526  dfiin2g  5036  iunss  5049  ralxfr2d  5409  ssrel2  5786  reliun  5817  idrefALT  6113  dfpo2  6296  funimass4  6957  fnssintima  7359  ralrnmpo  7547  imaeqalov  7646  ttrclss  9715  kmlem12  10156  fimaxre3  12160  gcdcllem1  16440  vdwmc2  16912  iunocv  21234  islindf4  21393  ovolgelb  24997  dyadmax  25115  itg2leub  25252  eqscut2  27307  addsprop  27460  addsuniflem  27484  negsprop  27509  mulsprop  27586  mulsuniflem  27604  mptelee  28153  nmoubi  30025  nmopub  31161  nmfnleub  31178  sigaclcu2  33118  untuni  34678  elintfv  34736  heibor1lem  36677  ispsubsp2  38617  pmapglbx  38640  neik0pk1imk0  42798  2reuimp0  45822
  Copyright terms: Public domain W3C validator