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 3167
Description: Restricted quantifier version of 19.21v 1940. (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 392 . . . 4 ((𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → (𝑥𝐴𝜓)))
21albii 1821 . . 3 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ ∀𝑥(𝜑 → (𝑥𝐴𝜓)))
3 19.21v 1940 . . 3 (∀𝑥(𝜑 → (𝑥𝐴𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
42, 3bitri 278 . 2 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
5 df-ral 3135 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝜓)))
6 df-ral 3135 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
76imbi2i 339 . 2 ((𝜑 → ∀𝑥𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
84, 5, 73bitr4i 306 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1536  wcel 2114  wral 3130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-ex 1782  df-ral 3135
This theorem is referenced by:  r19.23v  3265  r19.32v  3322  rmo4  3696  2reu5lem3  3723  ra4v  3841  rmo3  3845  dftr5  5151  reusv3  5283  tfinds2  7563  tfinds3  7564  wfr3g  7940  tfrlem1  7999  tfr3  8022  oeordi  8200  ordiso2  8967  ordtypelem7  8976  cantnf  9144  dfac12lem3  9560  ttukeylem5  9924  ttukeylem6  9925  fpwwe2lem8  10048  grudomon  10228  raluz2  12285  bpolycl  15397  ndvdssub  15749  gcdcllem1  15837  acsfn2  16925  pgpfac1  19193  pgpfac  19197  isdomn2  20063  islindf4  20525  isclo2  21691  1stccn  22066  kgencn  22159  txflf  22609  fclsopn  22617  nn0min  30546  bnj580  32259  bnj852  32267  rdgprc  33113  fpr3g  33196  conway  33338  filnetlem4  33803  poimirlem29  35044  heicant  35050  ntrneixb  40731  2rexrsb  43596  tfis2d  45149
  Copyright terms: Public domain W3C validator