Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.21v Structured version   Visualization version   GIF version

Theorem r19.21v 2943
 Description: Restricted quantifier version of 19.21v 1855. (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 1737 . . 3 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ ∀𝑥(𝜑 → (𝑥𝐴𝜓)))
3 19.21v 1855 . . 3 (∀𝑥(𝜑 → (𝑥𝐴𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
42, 3bitri 263 . 2 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
5 df-ral 2901 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝜓)))
6 df-ral 2901 . . 3 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
76imbi2i 325 . 2 ((𝜑 → ∀𝑥𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥𝐴𝜓)))
84, 5, 73bitr4i 291 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   ∈ wcel 1977  ∀wral 2896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827 This theorem depends on definitions:  df-bi 196  df-ex 1696  df-ral 2901 This theorem is referenced by:  r19.23v  3005  r19.32v  3064  rmo4  3366  2reu5lem3  3382  ra4v  3490  rmo3  3494  dftr5  4683  reusv3  4802  tfinds2  6955  tfinds3  6956  wfr3g  7300  tfrlem1  7359  tfr3  7382  oeordi  7554  ordiso2  8303  ordtypelem7  8312  cantnf  8473  dfac12lem3  8850  ttukeylem5  9218  ttukeylem6  9219  fpwwe2lem8  9338  grudomon  9518  raluz2  11613  bpolycl  14622  ndvdssub  14971  gcdcllem1  15059  acsfn2  16147  pgpfac1  18302  pgpfac  18306  isdomn2  19120  islindf4  19996  isclo2  20702  1stccn  21076  kgencn  21169  txflf  21620  fclsopn  21628  nn0min  28954  bnj580  30237  bnj852  30245  rdgprc  30944  filnetlem4  31546  poimirlem29  32608  heicant  32614  ntrneixb  37413  2rexrsb  39820  tfis2d  42225
 Copyright terms: Public domain W3C validator