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 3165
Description: Restricted quantifier version of 19.26 1872. (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 486 . . . 4 ((𝜑𝜓) → 𝜑)
21ralimi 3155 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜑)
3 simpr 488 . . . 4 ((𝜑𝜓) → 𝜓)
43ralimi 3155 . . 3 (∀𝑥𝐴 (𝜑𝜓) → ∀𝑥𝐴 𝜓)
52, 4jca 515 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
6 pm3.2 473 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
76ral2imi 3151 . . 3 (∀𝑥𝐴 𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 (𝜑𝜓)))
87imp 410 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∀𝑥𝐴 (𝜑𝜓))
95, 8impbii 212 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wral 3133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3138
This theorem is referenced by:  r19.26-2  3166  r19.26-3  3167  ralbiim  3169  r19.27v  3179  r19.27vOLD  3180  r19.28v  3181  reu8  3710  ssrab  4035  r19.28z  4426  r19.27z  4433  ralnralall  4441  2reu4lem  4448  2ralunsn  4811  iuneq2  4924  disjxun  5050  triin  5173  asymref2  5964  cnvpo  6125  fncnv  6415  fnres  6463  mptfnf  6472  fnopabg  6474  mpteqb  6778  eqfnfv3  6795  fvn0ssdmfun  6833  caoftrn  7438  wfr3g  7949  iiner  8365  ixpeq2  8471  ixpin  8483  ixpfi2  8819  wemaplem2  9008  dfac5  9552  kmlem6  9579  eltsk2g  10171  intgru  10234  axgroth6  10248  fsequb  13347  rexanuz  14705  rexanre  14706  cau3lem  14714  rlimcn2  14947  o1of2  14969  o1rlimmul  14975  climbdd  15028  sqrt2irr  15602  gcdcllem1  15846  pc11  16214  prmreclem2  16251  catpropd  16979  issubc3  17119  fucinv  17243  ispos2  17558  issubg3  18297  issubg4  18298  pmtrdifwrdel2  18614  ringsrg  19342  iunocv  20377  cply1mul  20930  scmatf1  21143  cpmatsubgpmat  21331  tgval2  21567  1stcelcls  22072  ptclsg  22226  ptcnplem  22232  fbun  22451  txflf  22617  ucncn  22897  prdsmet  22983  metequiv  23122  metequiv2  23123  ncvsi  23762  iscau4  23889  cmetcaulem  23898  evthicc2  24070  ismbfcn  24239  mbfi1flimlem  24332  rolle  24599  itgsubst  24658  plydivex  24899  ulmcaulem  24995  ulmcau  24996  ulmbdd  24999  ulmcn  25000  mumullem2  25771  2sqlem6  26013  tgcgr4  26331  axpasch  26741  axeuclid  26763  axcontlem2  26765  axcontlem4  26767  axcontlem7  26770  vtxd0nedgb  27284  fusgrregdegfi  27365  rusgr1vtxlem  27383  uspgr2wlkeq  27441  wlkdlem4  27481  lfgriswlk  27484  frgrreg  28185  frgrregord013  28186  friendshipgt3  28189  ocsh  29072  spanuni  29333  riesz4i  29852  leopadd  29921  leoptri  29925  leoptr  29926  inpr0  30306  disjunsn  30358  voliune  31548  volfiniune  31549  eulerpartlemr  31692  eulerpartlemn  31699  fmlasucdisj  32706  dfpo2  33051  poseq  33155  wzel  33171  frr3g  33181  ssltun2  33330  neibastop1  33767  phpreu  34989  ptrecube  35005  poimirlem23  35028  poimirlem27  35032  ovoliunnfl  35047  voliunnfl  35049  volsupnfl  35050  itg2addnc  35059  inixp  35114  rngoueqz  35326  intidl  35415  pclclN  37135  tendoeq2  38018  mzpincl  39595  lerabdioph  39666  ltrabdioph  39669  nerabdioph  39670  dvdsrabdioph  39671  dford3lem1  39887  gneispace  40760  ssrabf  41676  climxrre  42322  stoweidlem7  42579  stoweidlem54  42626  dirkercncflem3  42677  2ralbiim  43590  ply1mulgsumlem1  44724  ldepsnlinclem1  44844  ldepsnlinclem2  44845
  Copyright terms: Public domain W3C validator