Theorem mprgbir 3074

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

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

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

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

This theorem is referenced by:  ss2rabi  4100  ssintub  4990  djussxp  5870  dmiin  5978  dfco2  6276  coiun  6287  tron  6418  onxpdisj  6521  epweon  7810  frrlem6  8332  frrlem7  8333  wfrrelOLD  8370  wfrdmssOLD  8371  tfrlem6  8438  oawordeulem  8610  sbthlem1  9149  marypha2lem1  9504  ttrclselem1  9794  rankval4  9936  tcwf  9952  inlresf  9983  inrresf  9985  fin23lem16  10404  fin23lem29  10410  fin23lem30  10411  itunitc  10490  acncc  10509  wfgru  10885  renfdisj  11350  ioomax  13482  iccmax  13483  hashgval2  14427  fsumcom2  15822  fprodcom2  16032  dfphi2  16821  oppccatf  17788  dmcoass  18133  letsr  18663  smndex2dnrinv  18950  efgsf  19771  lssuni  20960  lpival  21357  cnsubdrglem  21459  retos  21659  psr1baslem  22207  istopon  22939  neips  23142  filssufilg  23940  xrhmeo  24996  iscmet3i  25365  ehlbase  25468  ovolge0  25535  unidmvol  25595  resinf1o  26596  divlogrlim  26695  dvloglem  26708  logf1o2  26710  atansssdm  26994  ppiub  27266  bday1s  27894  lrrecse  27993  clwwlkn0  30060  sspval  30755  shintcli  31361  lnopco0i  32036  imaelshi  32090  nmopadjlem  32121  nmoptrii  32126  nmopcoi  32127  nmopcoadji  32133  idleop  32163  hmopidmchi  32183  hmopidmpji  32184  djussxp2  32666  xrsclat  32994  rearchi  33339  dmvlsiga  34093  sxbrsigalem0  34236  dya2iocucvr  34249  eulerpartlemgh  34343  bnj110  34834  subfacp1lem1  35147  erdszelem2  35160  dfon2lem3  35749  filnetlem2  36345  taupi  37289  cnviun  43612  coiun1  43614  comptiunov2i  43668  cotrcltrcl  43687  cotrclrcl  43704  ssrab2f  45019  iooinlbub  45419  stirlinglem14  46008  sssalgen  46256  fvmptrabdm  47208  unilbss  48549