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  4361  iuneq2  4473  disjxun  4581  asymref2  5432  cnvpo  5590  fncnv  5876  fnres  5921  mptfnf  5928  fnopabg  5930  mpteqb  6207  eqfnfv3  6221  fvn0ssdmfun  6258  caoftrn  6830  wfr3g  7300  iiner  7706  ixpeq2  7808  ixpin  7819  ixpfi2  8147  wemaplem2  8335  dfac5  8834  kmlem6  8860  eltsk2g  9452  intgru  9515  axgroth6  9529  fsequb  12636  rexanuz  13933  rexanre  13934  cau3lem  13942  rlimcn2  14169  o1of2  14191  o1rlimmul  14197  climbdd  14250  sqrt2irr  14817  gcdcllem1  15059  pc11  15422  prmreclem2  15459  catpropd  16192  issubc3  16332  fucinv  16456  ispos2  16771  issubg3  17435  issubg4  17436  pmtrdifwrdel2  17729  ringsrg  18412  cply1mul  19485  iunocv  19844  scmatf1  20156  cpmatsubgpmat  20344  tgval2  20571  1stcelcls  21074  ptclsg  21228  ptcnplem  21234  fbun  21454  txflf  21620  ucncn  21899  prdsmet  21985  metequiv  22124  metequiv2  22125  ncvsi  22759  iscau4  22885  cmetcaulem  22894  evthicc2  23036  ismbfcn  23204  mbfi1flimlem  23295  rolle  23557  itgsubst  23616  plydivex  23856  ulmcaulem  23952  ulmcau  23953  ulmbdd  23956  ulmcn  23957  mumullem2  24706  2sqlem6  24948  tgcgr4  25226  axpasch  25621  axeuclid  25643  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  usg2wlkeq  26236  usgfiregdegfi  26438  usgreghash2spot  26596  frgrareg  26644  frgraregord013  26645  friendshipgt3  26648  ocsh  27526  spanuni  27787  riesz4i  28306  leopadd  28375  leoptri  28379  leoptr  28380  disjunsn  28789  voliune  29619  volfiniune  29620  eulerpartlemr  29763  eulerpartlemn  29770  dfpo2  30898  poseq  30994  wzel  31015  wzelOLD  31016  frr3g  31023  neibastop1  31524  phpreu  32563  ptrecube  32579  poimirlem23  32602  poimirlem27  32606  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  itg2addnc  32634  inixp  32693  rngoueqz  32909  intidl  32998  pclclN  34195  tendoeq2  35080  mzpincl  36315  lerabdioph  36387  ltrabdioph  36390  nerabdioph  36391  dvdsrabdioph  36392  dford3lem1  36611  gneispace  37452  ssrabf  38329  stoweidlem7  38900  stoweidlem54  38947  dirkercncflem3  38998  2ralbiim  39823  2reu4a  39838  ralnralall  40307  vtxd0nedgb  40703  fusgrregdegfi  40769  rusgr1vtxlem  40787  uspgr2wlkeq  40854  1wlkdlem4  40894  lfgriswlk  40897  fusgreghash2wsp  41502  av-frgrareg  41548  av-frgraregord013  41549  av-friendshipgt3  41552  ply1mulgsumlem1  41968  ldepsnlinclem1  42088  ldepsnlinclem2  42089  ssdifsn  42228
  Copyright terms: Public domain W3C validator