MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.21v Structured version   Visualization version   GIF version

Theorem r19.21v 2956
Description: Restricted quantifier version of 19.21v 1865. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.)
Assertion
Ref Expression
r19.21v (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.21v
StepHypRef Expression
1 bi2.04 376 . . . 4 ((𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → (𝑥𝐴𝜓)))
21albii 1744 . . 3 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ ∀𝑥(𝜑 → (𝑥𝐴𝜓)))
3 19.21v 1865 . . 3 (∀𝑥(𝜑 → (𝑥𝐴𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
42, 3bitri 264 . 2 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
5 df-ral 2913 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝜓)))
6 df-ral 2913 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
76imbi2i 326 . 2 ((𝜑 → ∀𝑥𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
84, 5, 73bitr4i 292 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1478  wcel 1987  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-ral 2913
This theorem is referenced by:  r19.23v  3018  r19.32v  3077  rmo4  3386  2reu5lem3  3402  ra4v  3510  rmo3  3514  dftr5  4725  reusv3  4846  tfinds2  7025  tfinds3  7026  wfr3g  7373  tfrlem1  7432  tfr3  7455  oeordi  7627  ordiso2  8380  ordtypelem7  8389  cantnf  8550  dfac12lem3  8927  ttukeylem5  9295  ttukeylem6  9296  fpwwe2lem8  9419  grudomon  9599  raluz2  11697  bpolycl  14727  ndvdssub  15076  gcdcllem1  15164  acsfn2  16264  pgpfac1  18419  pgpfac  18423  isdomn2  19239  islindf4  20117  isclo2  20832  1stccn  21206  kgencn  21299  txflf  21750  fclsopn  21758  nn0min  29450  bnj580  30744  bnj852  30752  rdgprc  31454  filnetlem4  32071  poimirlem29  33109  heicant  33115  ntrneixb  37914  2rexrsb  40505  tfis2d  41749
  Copyright terms: Public domain W3C validator