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 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
StepHypRef Expression
1 con34b 316 . . 3 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
21ralbii 3092 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴𝜓 → ¬ 𝜑))
3 r19.21v 3179 . 2 (∀𝑥𝐴𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
4 dfrex2 3072 . . . 4 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
54imbi1i 349 . . 3 ((∃𝑥𝐴 𝜑𝜓) ↔ (¬ ∀𝑥𝐴 ¬ 𝜑𝜓))
6 con1b 358 . . 3 ((¬ ∀𝑥𝐴 ¬ 𝜑𝜓) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
75, 6bitr2i 276 . 2 ((¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑) ↔ (∃𝑥𝐴 𝜑𝜓))
82, 3, 73bitri 297 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator