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 2114  ∀wral 3051

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

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

This theorem is referenced by:  ssintub  4908  djussxp  5800  dmiin  5908  dfco2  6209  coiun  6221  tron  6346  onxpdisj  6450  epweon  7729  frrlem6  8241  frrlem7  8242  tfrlem6  8321  oawordeulem  8489  sbthlem1  9025  marypha2lem1  9348  ttrclselem1  9646  rankval4  9791  tcwf  9807  inlresf  9838  inrresf  9840  fin23lem16  10257  fin23lem29  10263  fin23lem30  10264  itunitc  10343  acncc  10362  wfgru  10739  renfdisj  11205  ioomax  13375  iccmax  13376  hashgval2  14340  fsumcom2  15736  fprodcom2  15949  dfphi2  16744  oppccatf  17694  dmcoass  18033  letsr  18559  smndex2dnrinv  18886  efgsf  19704  lssuni  20934  lpival  21322  cnsubdrglem  21398  retos  21598  psr1baslem  22148  istopon  22877  neips  23078  filssufilg  23876  xrhmeo  24913  iscmet3i  25279  ehlbase  25382  ovolge0  25448  unidmvol  25508  resinf1o  26500  divlogrlim  26599  dvloglem  26612  logf1o2  26614  atansssdm  26897  ppiub  27167  bday1  27806  lrrecse  27934  clwwlkn0  30098  sspval  30794  shintcli  31400  lnopco0i  32075  imaelshi  32129  nmopadjlem  32160  nmoptrii  32165  nmopcoi  32166  nmopcoadji  32172  idleop  32202  hmopidmchi  32222  hmopidmpji  32223  djussxp2  32721  xrsclat  33071  rearchi  33406  dmvlsiga  34273  sxbrsigalem0  34415  dya2iocucvr  34428  eulerpartlemgh  34522  bnj110  35000  subfacp1lem1  35361  erdszelem2  35374  dfon2lem3  35965  filnetlem2  36561  ttciunun  36693  taupi  37637  cnviun  44077  coiun1  44079  comptiunov2i  44133  cotrcltrcl  44152  cotrclrcl  44169  ssrab2f  45547  iooinlbub  45931  stirlinglem14  46515  sssalgen  46763  fvmptrabdm  47741  stgr0  48436  unilbss  49293  dfinito4  49976