Theorem mprgbir 3058

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 3053	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝜓
3		mprgbir.1	. 2 ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)
4	2, 3	mpbir 231	1 ⊢ 𝜑

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  ∀wral 3051

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 3052

This theorem is referenced by:  ss2rabi  4052  ssintub  4942  djussxp  5825  dmiin  5933  dfco2  6234  coiun  6245  tron  6375  onxpdisj  6480  epweon  7769  frrlem6  8290  frrlem7  8291  wfrrelOLD  8328  wfrdmssOLD  8329  tfrlem6  8396  oawordeulem  8566  sbthlem1  9097  marypha2lem1  9447  ttrclselem1  9739  rankval4  9881  tcwf  9897  inlresf  9928  inrresf  9930  fin23lem16  10349  fin23lem29  10355  fin23lem30  10356  itunitc  10435  acncc  10454  wfgru  10830  renfdisj  11295  ioomax  13439  iccmax  13440  hashgval2  14396  fsumcom2  15790  fprodcom2  16000  dfphi2  16793  oppccatf  17740  dmcoass  18079  letsr  18603  smndex2dnrinv  18893  efgsf  19710  lssuni  20896  lpival  21285  cnsubdrglem  21386  retos  21578  psr1baslem  22120  istopon  22850  neips  23051  filssufilg  23849  xrhmeo  24895  iscmet3i  25264  ehlbase  25367  ovolge0  25434  unidmvol  25494  resinf1o  26497  divlogrlim  26596  dvloglem  26609  logf1o2  26611  atansssdm  26895  ppiub  27167  bday1s  27795  lrrecse  27901  clwwlkn0  30009  sspval  30704  shintcli  31310  lnopco0i  31985  imaelshi  32039  nmopadjlem  32070  nmoptrii  32075  nmopcoi  32076  nmopcoadji  32082  idleop  32112  hmopidmchi  32132  hmopidmpji  32133  djussxp2  32626  xrsclat  33003  rearchi  33361  dmvlsiga  34160  sxbrsigalem0  34303  dya2iocucvr  34316  eulerpartlemgh  34410  bnj110  34889  subfacp1lem1  35201  erdszelem2  35214  dfon2lem3  35803  filnetlem2  36397  taupi  37341  cnviun  43674  coiun1  43676  comptiunov2i  43730  cotrcltrcl  43749  cotrclrcl  43766  ssrab2f  45141  iooinlbub  45530  stirlinglem14  46116  sssalgen  46364  fvmptrabdm  47322  stgr0  47972  unilbss  48796  dfinito4  49386