Theorem mprgbir 3088

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ral 3082

This theorem is used by:  ssintub  4933  djussxp  5833  dmiin  5945  dfco2  6248  coiun  6260  tron  6387  onxpdisj  6492  epweon  7780  frrlem6  8294  frrlem7  8295  tfrlem6OLD  8375  oawordeulem  8545  sbthlem1  9082  marypha2lem1  9402  ttrclselem1  9701  rankval4  9846  tcwf  9862  inlresf  9916  inrresf  9918  fin23lem16  10334  fin23lem29  10340  fin23lem30  10341  itunitc  10420  acncc  10439  wfgru  10818  renfdisj  11286  ioomax  13467  iccmax  13468  hashgval2  14434  fsumcom2  15850  fprodcom2  16063  dfphi2  16857  oppccatf  17808  dmcoass  18147  letsr  18673  smndex2dnrinv  19016  efgsf  19845  lssuni  21112  lpival  21544  cnsubdrglem  21620  retos  21820  psr1baslem  22397  istopon  23121  neips  23322  filssufilg  24121  xrhmeo  25158  iscmet3i  25524  ehlbase  25627  ovolge0  25693  unidmvol  25753  resinf1o  26754  divlogrlim  26853  dvloglem  26866  logf1o2  26868  atansssdm  27151  ppiub  27421  bday1  28060  lrrecse  28188  clwwlkn0  30448  sspval  31148  shintcli  31754  lnopco0i  32429  imaelshi  32483  nmopadjlem  32514  nmoptrii  32519  nmopcoi  32520  nmopcoadji  32526  idleop  32556  hmopidmchi  32576  hmopidmpji  32577  djussxp2  33066  xrsclat  33397  rearchi  33732  dmvlsiga  34585  sxbrsigalem0  34728  dya2iocucvr  34741  eulerpartlemgh  34835  bnj110  35313  subfacp1lem1  35710  erdszelem2  35723  dfon2lem3  36314  filnetlem2  36949  ttciunun  37081  taupi  38026  cnviun  44436  coiun1  44438  comptiunov2i  44492  cotrcltrcl  44511  cotrclrcl  44528  ssrab2f  45895  iooinlbub  46277  stirlinglem14  46861  sssalgen  47109  fvmptrabdm  48090  stgr0  48785  unilbss  49655  dfinito4  50338