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 3176
Description: Restricted quantifier version of 19.23v 1946. Version of r19.23 3238 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 3093 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴𝜓 → ¬ 𝜑))
3 r19.21v 3173 . 2 (∀𝑥𝐴𝜓 → ¬ 𝜑) ↔ (¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
4 dfrex2 3073 . . . 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 3061  wrex 3070
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 3062  df-rex 3071
This theorem is referenced by:  rexlimivOLD  3178  ceqsralv  3482  ralxpxfr2d  3597  uniiunlem  4045  2reu4lem  4484  dfiin2g  4993  iunss  5006  ralxfr2d  5366  ssrel2  5742  reliun  5773  idrefALT  6066  dfpo2  6249  funimass4  6908  fnssintima  7308  ralrnmpo  7495  imaeqalov  7594  ttrclss  9661  kmlem12  10102  fimaxre3  12106  gcdcllem1  16384  vdwmc2  16856  iunocv  21101  islindf4  21260  ovolgelb  24860  dyadmax  24978  itg2leub  25115  eqscut2  27167  addsprop  27310  addsunif  27332  negsprop  27355  mptelee  27886  nmoubi  29756  nmopub  30892  nmfnleub  30909  sigaclcu2  32776  untuni  34337  elintfv  34395  heibor1lem  36314  ispsubsp2  38255  pmapglbx  38278  neik0pk1imk0  42407  2reuimp0  45432
  Copyright terms: Public domain W3C validator