Theorem mprgbir 3056

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  ∀wral 3049

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

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

This theorem is referenced by:  ssintub  4919  djussxp  5792  dmiin  5900  dfco2  6201  coiun  6213  tron  6338  onxpdisj  6442  epweon  7718  frrlem6  8231  frrlem7  8232  tfrlem6  8311  oawordeulem  8479  sbthlem1  9013  marypha2lem1  9336  ttrclselem1  9632  rankval4  9777  tcwf  9793  inlresf  9824  inrresf  9826  fin23lem16  10243  fin23lem29  10249  fin23lem30  10250  itunitc  10329  acncc  10348  wfgru  10725  renfdisj  11190  ioomax  13336  iccmax  13337  hashgval2  14299  fsumcom2  15695  fprodcom2  15905  dfphi2  16699  oppccatf  17649  dmcoass  17988  letsr  18514  smndex2dnrinv  18838  efgsf  19656  lssuni  20888  lpival  21277  cnsubdrglem  21371  retos  21571  psr1baslem  22123  istopon  22854  neips  23055  filssufilg  23853  xrhmeo  24898  iscmet3i  25266  ehlbase  25369  ovolge0  25436  unidmvol  25496  resinf1o  26499  divlogrlim  26598  dvloglem  26611  logf1o2  26613  atansssdm  26897  ppiub  27169  bday1s  27802  lrrecse  27912  clwwlkn0  30052  sspval  30747  shintcli  31353  lnopco0i  32028  imaelshi  32082  nmopadjlem  32113  nmoptrii  32118  nmopcoi  32119  nmopcoadji  32125  idleop  32155  hmopidmchi  32175  hmopidmpji  32176  djussxp2  32675  xrsclat  33042  rearchi  33376  dmvlsiga  34235  sxbrsigalem0  34377  dya2iocucvr  34390  eulerpartlemgh  34484  bnj110  34963  subfacp1lem1  35322  erdszelem2  35335  dfon2lem3  35926  filnetlem2  36522  taupi  37467  cnviun  43833  coiun1  43835  comptiunov2i  43889  cotrcltrcl  43908  cotrclrcl  43925  ssrab2f  45303  iooinlbub  45689  stirlinglem14  46273  sssalgen  46521  fvmptrabdm  47481  stgr0  48148  unilbss  49005  dfinito4  49688