Theorem mprgbir 3051

Description: Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)

Hypotheses

Ref	Expression
mprgbir.1	⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
mprgbir.2	⊢ (𝑥 ∈ 𝐴 → 𝜓)

Assertion

Ref	Expression
mprgbir	⊢ 𝜑

Proof of Theorem mprgbir

Step	Hyp	Ref	Expression
1		mprgbir.2	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝜓)
2	1	rgen 3046	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓
3		mprgbir.1	. 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
4	2, 3	mpbir 231	1 ⊢ 𝜑

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795

This theorem depends on definitions:  df-bi 207  df-ral 3045

This theorem is referenced by:  ss2rabi  4040  ssintub  4930  djussxp  5809  dmiin  5917  dfco2  6218  coiun  6229  tron  6355  onxpdisj  6460  epweon  7751  frrlem6  8270  frrlem7  8271  tfrlem6  8350  oawordeulem  8518  sbthlem1  9051  marypha2lem1  9386  ttrclselem1  9678  rankval4  9820  tcwf  9836  inlresf  9867  inrresf  9869  fin23lem16  10288  fin23lem29  10294  fin23lem30  10295  itunitc  10374  acncc  10393  wfgru  10769  renfdisj  11234  ioomax  13383  iccmax  13384  hashgval2  14343  fsumcom2  15740  fprodcom2  15950  dfphi2  16744  oppccatf  17689  dmcoass  18028  letsr  18552  smndex2dnrinv  18842  efgsf  19659  lssuni  20845  lpival  21234  cnsubdrglem  21335  retos  21527  psr1baslem  22069  istopon  22799  neips  23000  filssufilg  23798  xrhmeo  24844  iscmet3i  25212  ehlbase  25315  ovolge0  25382  unidmvol  25442  resinf1o  26445  divlogrlim  26544  dvloglem  26557  logf1o2  26559  atansssdm  26843  ppiub  27115  bday1s  27743  lrrecse  27849  clwwlkn0  29957  sspval  30652  shintcli  31258  lnopco0i  31933  imaelshi  31987  nmopadjlem  32018  nmoptrii  32023  nmopcoi  32024  nmopcoadji  32030  idleop  32060  hmopidmchi  32080  hmopidmpji  32081  djussxp2  32572  xrsclat  32949  rearchi  33317  dmvlsiga  34119  sxbrsigalem0  34262  dya2iocucvr  34275  eulerpartlemgh  34369  bnj110  34848  subfacp1lem1  35166  erdszelem2  35179  dfon2lem3  35773  filnetlem2  36367  taupi  37311  cnviun  43639  coiun1  43641  comptiunov2i  43695  cotrcltrcl  43714  cotrclrcl  43731  ssrab2f  45111  iooinlbub  45499  stirlinglem14  46085  sssalgen  46333  fvmptrabdm  47294  stgr0  47959  unilbss  48806  dfinito4  49490