Theorem mprgbir 3066

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2104  ∀wral 3059

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 206  df-ral 3060

This theorem is referenced by:  ss2rabi  4073  rabxm  4385  ssintub  4969  djussxp  5844  dmiin  5951  dfco2  6243  coiun  6254  tron  6386  onxpdisj  6489  epweon  7764  frrlem6  8278  frrlem7  8279  wfrrelOLD  8316  wfrdmssOLD  8317  tfrlem6  8384  oawordeulem  8556  sbthlem1  9085  marypha2lem1  9432  ttrclselem1  9722  rankval4  9864  tcwf  9880  inlresf  9911  inrresf  9913  fin23lem16  10332  fin23lem29  10338  fin23lem30  10339  itunitc  10418  acncc  10437  wfgru  10813  renfdisj  11278  ioomax  13403  iccmax  13404  hashgval2  14342  fsumcom2  15724  fprodcom2  15932  dfphi2  16711  oppccatf  17678  dmcoass  18020  letsr  18550  smndex2dnrinv  18832  efgsf  19638  lssuni  20694  lpival  21083  cnsubdrglem  21196  retos  21390  psr1baslem  21928  istopon  22634  neips  22837  filssufilg  23635  xrhmeo  24691  iscmet3i  25060  ehlbase  25163  ovolge0  25230  unidmvol  25290  resinf1o  26281  divlogrlim  26379  dvloglem  26392  logf1o2  26394  atansssdm  26674  ppiub  26943  bday1s  27569  lrrecse  27664  clwwlkn0  29548  sspval  30243  shintcli  30849  lnopco0i  31524  imaelshi  31578  nmopadjlem  31609  nmoptrii  31614  nmopcoi  31615  nmopcoadji  31621  idleop  31651  hmopidmchi  31671  hmopidmpji  31672  djussxp2  32140  xrsclat  32448  rearchi  32731  dmvlsiga  33425  sxbrsigalem0  33568  dya2iocucvr  33581  eulerpartlemgh  33675  bnj110  34167  subfacp1lem1  34468  erdszelem2  34481  dfon2lem3  35061  filnetlem2  35567  taupi  36507  cnviun  42703  coiun1  42705  comptiunov2i  42759  cotrcltrcl  42778  cotrclrcl  42795  ssrab2f  44107  iooinlbub  44512  stirlinglem14  45101  sssalgen  45349  fvmptrabdm  46299  unilbss  47589