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 3224
Description: Restricted quantifier version of 19.23v 1901. Version of r19.23 3257 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 308 . . 3 ((𝜑𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
21ralbii 3115 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴𝜓 → ¬ 𝜑))
3 r19.21v 3125 . 2 (∀𝑥𝐴𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
4 dfrex2 3186 . . . 4 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
54imbi1i 342 . . 3 ((∃𝑥𝐴 𝜑𝜓) ↔ (¬ ∀𝑥𝐴 ¬ 𝜑𝜓))
6 con1b 351 . . 3 ((¬ ∀𝑥𝐴 ¬ 𝜑𝜓) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
75, 6bitr2i 268 . 2 ((¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑) ↔ (∃𝑥𝐴 𝜑𝜓))
82, 3, 73bitri 289 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wral 3088  wrex 3089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-ral 3093  df-rex 3094
This theorem is referenced by:  rexlimiv  3225  ralxpxfr2d  3554  uniiunlem  3953  2reu4lem  4349  dfiin2g  4828  iunss  4836  ralxfr2d  5165  ssrel2  5510  reliun  5540  idrefALT  5815  funimass4  6562  ralrnmpo  7107  kmlem12  9383  fimaxre3  11390  gcdcllem1  15711  vdwmc2  16174  iunocv  20530  islindf4  20687  ovolgelb  23787  dyadmax  23905  itg2leub  24041  mptelee  26387  nmoubi  28329  nmopub  29469  nmfnleub  29486  sigaclcu2  31024  untuni  32455  dfpo2  32511  elintfv  32527  heibor1lem  34529  ispsubsp2  36327  pmapglbx  36350  neik0pk1imk0  39760  2reuimp0  42720
  Copyright terms: Public domain W3C validator