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

Theorem r19.26 3046
Description: Restricted quantifier version of 19.26 1786. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.26 (∀𝑥𝐴 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))

Proof of Theorem r19.26
StepHypRef Expression
1 simpl 472 . . . 4 ((𝜑𝜓) → 𝜑)
21ralimi 2936 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜑)
3 simpr 476 . . . 4 ((𝜑𝜓) → 𝜓)
43ralimi 2936 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜓)
52, 4jca 553 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
6 pm3.2 462 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76ral2imi 2931 . . 3 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 (𝜑𝜓)))
87imp 444 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∀𝑥𝐴 (𝜑𝜓))
95, 8impbii 198 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383  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
This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901
This theorem is referenced by:  r19.26-2  3047  r19.26-3  3048  ralbiim  3051  r19.27v  3052  r19.35  3065  reu8  3369  ssrab  3643  r19.28z  4015  r19.27z  4022  2ralunsn  4356  iuneq2  4468  disjxun  4576  asymref2  5419  cnvpo  5576  fncnv  5862  fnres  5907  mptfnf  5914  fnopabg  5916  mpteqb  6192  eqfnfv3  6206  fvn0ssdmfun  6243  caoftrn  6808  wfr3g  7278  iiner  7684  ixpeq2  7786  ixpin  7797  ixpfi2  8125  wemaplem2  8313  dfac5  8812  kmlem6  8838  eltsk2g  9430  intgru  9493  axgroth6  9507  fsequb  12594  rexanuz  13882  rexanre  13883  cau3lem  13891  rlimcn2  14118  o1of2  14140  o1rlimmul  14146  climbdd  14199  sqrt2irr  14766  gcdcllem1  15008  pc11  15371  prmreclem2  15408  catpropd  16141  issubc3  16281  fucinv  16405  ispos2  16720  issubg3  17384  issubg4  17385  pmtrdifwrdel2  17678  ringsrg  18361  cply1mul  19434  iunocv  19792  scmatf1  20104  cpmatsubgpmat  20292  tgval2  20519  1stcelcls  21022  ptclsg  21176  ptcnplem  21182  fbun  21402  txflf  21568  ucncn  21847  prdsmet  21933  metequiv  22072  metequiv2  22073  ncvsi  22704  iscau4  22830  cmetcaulem  22839  evthicc2  22981  ismbfcn  23149  mbfi1flimlem  23240  rolle  23502  itgsubst  23561  plydivex  23801  ulmcaulem  23897  ulmcau  23898  ulmbdd  23901  ulmcn  23902  mumullem2  24651  2sqlem6  24893  tgcgr4  25172  axpasch  25567  axeuclid  25589  axcontlem2  25591  axcontlem4  25593  axcontlem7  25596  usg2wlkeq  26030  usgfiregdegfi  26232  usgreghash2spot  26390  frgrareg  26438  frgraregord013  26439  friendshipgt3  26442  ocsh  27320  spanuni  27581  riesz4i  28100  leopadd  28169  leoptri  28173  leoptr  28174  disjunsn  28583  voliune  29413  volfiniune  29414  eulerpartlemr  29557  eulerpartlemn  29564  dfpo2  30692  poseq  30788  wzel  30809  wzelOLD  30810  frr3g  30817  neibastop1  31318  phpreu  32357  ptrecube  32373  poimirlem23  32396  poimirlem27  32400  ovoliunnfl  32415  voliunnfl  32417  volsupnfl  32418  itg2addnc  32428  inixp  32487  rngoueqz  32703  intidl  32792  pclclN  33989  tendoeq2  34874  mzpincl  36109  lerabdioph  36181  ltrabdioph  36184  nerabdioph  36185  dvdsrabdioph  36186  dford3lem1  36405  gneispace  37246  ssrabf  38123  stoweidlem7  38694  stoweidlem54  38741  dirkercncflem3  38792  2ralbiim  39617  2reu4a  39632  ralnralall  40102  vtxd0nedgb  40695  fusgrregdegfi  40761  rusgr1vtxlem  40779  uspgr2wlkeq  40846  1wlkdlem4  40886  lfgriswlk  40889  fusgreghash2wsp  41494  av-frgrareg  41540  av-frgraregord013  41541  av-friendshipgt3  41544  ply1mulgsumlem1  41960  ldepsnlinclem1  42080  ldepsnlinclem2  42081
  Copyright terms: Public domain W3C validator