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 3175
Description: Restricted quantifier version of 19.21v 1931. (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 389 . . . 4 ((𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → (𝑥𝐴𝜓)))
21albii 1811 . . 3 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ ∀𝑥(𝜑 → (𝑥𝐴𝜓)))
3 19.21v 1931 . . 3 (∀𝑥(𝜑 → (𝑥𝐴𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
42, 3bitri 276 . 2 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
5 df-ral 3143 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝜓)))
6 df-ral 3143 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
76imbi2i 337 . 2 ((𝜑 → ∀𝑥𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
84, 5, 73bitr4i 304 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526  wcel 2105  wral 3138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-ex 1772  df-ral 3143
This theorem is referenced by:  r19.23v  3279  r19.32v  3340  rmo4  3720  2reu5lem3  3747  ra4v  3867  rmo3  3871  rmo3OLD  3872  dftr5  5167  reusv3  5297  tfinds2  7566  tfinds3  7567  wfr3g  7944  tfrlem1  8003  tfr3  8026  oeordi  8203  ordiso2  8968  ordtypelem7  8977  cantnf  9145  dfac12lem3  9560  ttukeylem5  9924  ttukeylem6  9925  fpwwe2lem8  10048  grudomon  10228  raluz2  12286  bpolycl  15396  ndvdssub  15750  gcdcllem1  15838  acsfn2  16924  pgpfac1  19133  pgpfac  19137  isdomn2  20002  islindf4  20912  isclo2  21626  1stccn  22001  kgencn  22094  txflf  22544  fclsopn  22552  nn0min  30464  bnj580  32085  bnj852  32093  rdgprc  32937  fpr3g  33020  conway  33162  filnetlem4  33627  poimirlem29  34803  heicant  34809  ntrneixb  40325  2rexrsb  43181  tfis2d  44681
  Copyright terms: Public domain W3C validator