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 2989
Description: Restricted quantifier version of 19.21v 1908. (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 375 . . . 4 ((𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → (𝑥𝐴𝜓)))
21albii 1787 . . 3 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ ∀𝑥(𝜑 → (𝑥𝐴𝜓)))
3 19.21v 1908 . . 3 (∀𝑥(𝜑 → (𝑥𝐴𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
42, 3bitri 264 . 2 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
5 df-ral 2946 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝜓)))
6 df-ral 2946 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
76imbi2i 325 . 2 ((𝜑 → ∀𝑥𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
84, 5, 73bitr4i 292 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-ral 2946
This theorem is referenced by:  r19.23v  3052  r19.32v  3112  rmo4  3432  2reu5lem3  3448  ra4v  3557  rmo3  3561  dftr5  4788  reusv3  4906  tfinds2  7105  tfinds3  7106  wfr3g  7458  tfrlem1  7517  tfr3  7540  oeordi  7712  ordiso2  8461  ordtypelem7  8470  cantnf  8628  dfac12lem3  9005  ttukeylem5  9373  ttukeylem6  9374  fpwwe2lem8  9497  grudomon  9677  raluz2  11775  bpolycl  14827  ndvdssub  15180  gcdcllem1  15268  acsfn2  16371  pgpfac1  18525  pgpfac  18529  isdomn2  19347  islindf4  20225  isclo2  20940  1stccn  21314  kgencn  21407  txflf  21857  fclsopn  21865  nn0min  29695  bnj580  31109  bnj852  31117  rdgprc  31824  conway  32035  filnetlem4  32501  poimirlem29  33568  heicant  33574  ntrneixb  38710  2rexrsb  41492  tfis2d  42752
  Copyright terms: Public domain W3C validator