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

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 3052

This theorem is referenced by:  ssintub  4921  djussxp  5794  dmiin  5902  dfco2  6203  coiun  6215  tron  6340  onxpdisj  6444  epweon  7720  frrlem6  8233  frrlem7  8234  tfrlem6  8313  oawordeulem  8481  sbthlem1  9017  marypha2lem1  9340  ttrclselem1  9636  rankval4  9781  tcwf  9797  inlresf  9828  inrresf  9830  fin23lem16  10247  fin23lem29  10253  fin23lem30  10254  itunitc  10333  acncc  10352  wfgru  10729  renfdisj  11194  ioomax  13340  iccmax  13341  hashgval2  14303  fsumcom2  15699  fprodcom2  15909  dfphi2  16703  oppccatf  17653  dmcoass  17992  letsr  18518  smndex2dnrinv  18842  efgsf  19660  lssuni  20892  lpival  21281  cnsubdrglem  21375  retos  21575  psr1baslem  22127  istopon  22858  neips  23059  filssufilg  23857  xrhmeo  24902  iscmet3i  25270  ehlbase  25373  ovolge0  25440  unidmvol  25500  resinf1o  26503  divlogrlim  26602  dvloglem  26615  logf1o2  26617  atansssdm  26901  ppiub  27173  bday1  27812  lrrecse  27940  clwwlkn0  30105  sspval  30800  shintcli  31406  lnopco0i  32081  imaelshi  32135  nmopadjlem  32166  nmoptrii  32171  nmopcoi  32172  nmopcoadji  32178  idleop  32208  hmopidmchi  32228  hmopidmpji  32229  djussxp2  32728  xrsclat  33095  rearchi  33429  dmvlsiga  34288  sxbrsigalem0  34430  dya2iocucvr  34443  eulerpartlemgh  34537  bnj110  35016  subfacp1lem1  35375  erdszelem2  35388  dfon2lem3  35979  filnetlem2  36575  taupi  37530  cnviun  43912  coiun1  43914  comptiunov2i  43968  cotrcltrcl  43987  cotrclrcl  44004  ssrab2f  45382  iooinlbub  45768  stirlinglem14  46352  sssalgen  46600  fvmptrabdm  47560  stgr0  48227  unilbss  49084  dfinito4  49767