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 3086
Description: Restricted quantifier version of 19.21v 2005. (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 1884 . . 3 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ ∀𝑥(𝜑 → (𝑥𝐴𝜓)))
3 19.21v 2005 . . 3 (∀𝑥(𝜑 → (𝑥𝐴𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
42, 3bitri 264 . 2 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
5 df-ral 3043 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝜓)))
6 df-ral 3043 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
76imbi2i 325 . 2 ((𝜑 → ∀𝑥𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
84, 5, 73bitr4i 292 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1618  wcel 2127  wral 3038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976
This theorem depends on definitions:  df-bi 197  df-ex 1842  df-ral 3043
This theorem is referenced by:  r19.23v  3149  r19.32v  3209  rmo4  3528  2reu5lem3  3544  ra4v  3653  rmo3  3657  dftr5  4895  reusv3  5013  tfinds2  7216  tfinds3  7217  wfr3g  7570  tfrlem1  7629  tfr3  7652  oeordi  7824  ordiso2  8573  ordtypelem7  8582  cantnf  8751  dfac12lem3  9130  ttukeylem5  9498  ttukeylem6  9499  fpwwe2lem8  9622  grudomon  9802  raluz2  11901  bpolycl  14953  ndvdssub  15306  gcdcllem1  15394  acsfn2  16496  pgpfac1  18650  pgpfac  18654  isdomn2  19472  islindf4  20350  isclo2  21065  1stccn  21439  kgencn  21532  txflf  21982  fclsopn  21990  nn0min  29847  bnj580  31261  bnj852  31269  rdgprc  31976  conway  32187  filnetlem4  32653  poimirlem29  33720  heicant  33726  ntrneixb  38864  2rexrsb  41646  tfis2d  42906
  Copyright terms: Public domain W3C validator