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 3189
Description: Restricted quantifier version of 19.21v 1968. (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.) (Proof shortened by Wolf Lammen, 11-Dec-2024.)
Assertion
Ref Expression
r19.21v (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.21v
StepHypRef Expression
1 pm2.27 43 . . . 4 (𝜑 → ((𝜑𝜓) → 𝜓))
21ralimdv 3178 . . 3 (𝜑 → (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜓))
32com12 33 . 2 (∀𝑥𝐴 (𝜑𝜓) → (𝜑 → ∀𝑥𝐴 𝜓))
4 pm2.21 124 . . . 4 𝜑 → (𝜑𝜓))
54ralrimivw 3160 . . 3 𝜑 → ∀𝑥𝐴 (𝜑𝜓))
6 ax-1 6 . . . 4 (𝜓 → (𝜑𝜓))
76ralimi 3101 . . 3 (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 (𝜑𝜓))
85, 7ja 188 . 2 ((𝜑 → ∀𝑥𝐴 𝜓) → ∀𝑥𝐴 (𝜑𝜓))
93, 8impbii 212 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3  wi 4  wb 209  wral 3078
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939
This proof depends on definitions:  df-bi 210  df-an 401  df-ral 3079
This theorem is used by:  r19.23v  3191  r19.32v  3197  cbvraldva  3244  rmo4  3692  2reu5lem3  3719  ra4v  3837  rmo3  3841  dftr5  5221  reusv3  5375  tfinds2  7858  tfinds3  7859  fpr3g  8280  wfr3g  8314  tfrlem1  8360  tfr3  8384  oeordi  8571  naddssim  8670  ordiso2  9475  ordtypelem7  9484  cantnf  9660  dfac12lem3  10136  ttukeylem5  10503  ttukeylem6  10504  fpwwe2lem7  10628  grudomon  10808  raluz2  12927  bpolycl  16112  ndvdssub  16473  gcdcllem1  16563  acsfn2  17725  pgpfac1  20158  pgpfac  20162  isdomn5  20820  islindf4  21999  isclo2  23256  1stccn  23631  kgencn  23724  txflf  24174  fclsopn  24182  conway  27983  nn0min  33176  bnj580  35310  bnj852  35318  rdgprc  36292  filnetlem4  36920  poimirlem29  38328  heicant  38334  indstrd  42988  ntrneixb  44849  trfr  45699  modelac8prim  45729  2rexrsb  47867  tfis2d  50486
  Copyright terms: Public domain W3C validator