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

Theorem r19.21v 3126
 Description: Restricted quantifier version of 19.21v 1898. (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 380 . . . 4 ((𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → (𝑥𝐴𝜓)))
21albii 1782 . . 3 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ ∀𝑥(𝜑 → (𝑥𝐴𝜓)))
3 19.21v 1898 . . 3 (∀𝑥(𝜑 → (𝑥𝐴𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
42, 3bitri 267 . 2 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
5 df-ral 3094 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝜓)))
6 df-ral 3094 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
76imbi2i 328 . 2 ((𝜑 → ∀𝑥𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
84, 5, 73bitr4i 295 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1505   ∈ wcel 2050  ∀wral 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-ex 1743  df-ral 3094 This theorem is referenced by:  r19.23v  3225  r19.32v  3282  rmo4  3634  2reu5lem3  3658  ra4v  3772  rmo3  3776  rmo3OLD  3777  dftr5  5033  reusv3  5159  tfinds2  7394  tfinds3  7395  wfr3g  7756  tfrlem1  7816  tfr3  7839  oeordi  8014  ordiso2  8774  ordtypelem7  8783  cantnf  8950  dfac12lem3  9365  ttukeylem5  9733  ttukeylem6  9734  fpwwe2lem8  9857  grudomon  10037  raluz2  12111  bpolycl  15266  ndvdssub  15620  gcdcllem1  15708  acsfn2  16792  pgpfac1  18952  pgpfac  18956  isdomn2  19793  islindf4  20684  isclo2  21400  1stccn  21775  kgencn  21868  txflf  22318  fclsopn  22326  nn0min  30283  bnj580  31829  bnj852  31837  rdgprc  32557  fpr3g  32640  conway  32782  filnetlem4  33247  poimirlem29  34359  heicant  34365  ntrneixb  39805  2rexrsb  42704  tfis2d  44148
 Copyright terms: Public domain W3C validator