Theorem mprgbir 3092

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2149  ∀wral 3085

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

This theorem depends on definitions:  df-bi 210  df-ral 3086

This theorem is referenced by:  ssintub  4935  djussxp  5832  dmiin  5944  dfco2  6247  coiun  6259  tron  6384  onxpdisj  6489  epweon  7774  frrlem6  8288  frrlem7  8289  tfrlem6OLD  8369  oawordeulem  8539  sbthlem1  9075  marypha2lem1  9395  ttrclselem1  9694  rankval4  9839  tcwf  9855  inlresf  9900  inrresf  9902  fin23lem16  10319  fin23lem29  10325  fin23lem30  10326  itunitc  10405  acncc  10424  wfgru  10801  renfdisj  11269  ioomax  13449  iccmax  13450  hashgval2  14414  fsumcom2  15825  fprodcom2  16038  dfphi2  16833  oppccatf  17784  dmcoass  18123  letsr  18649  smndex2dnrinv  18977  efgsf  19799  lssuni  21038  lpival  21461  cnsubdrglem  21537  retos  21737  psr1baslem  22314  istopon  23038  neips  23239  filssufilg  24037  xrhmeo  25074  iscmet3i  25440  ehlbase  25543  ovolge0  25609  unidmvol  25669  resinf1o  26667  divlogrlim  26766  dvloglem  26779  logf1o2  26781  atansssdm  27064  ppiub  27334  bday1  27973  lrrecse  28101  clwwlkn0  30320  sspval  31016  shintcli  31622  lnopco0i  32297  imaelshi  32351  nmopadjlem  32382  nmoptrii  32387  nmopcoi  32388  nmopcoadji  32394  idleop  32424  hmopidmchi  32444  hmopidmpji  32445  djussxp2  32934  xrsclat  33272  rearchi  33609  dmvlsiga  34464  sxbrsigalem0  34606  dya2iocucvr  34619  eulerpartlemgh  34713  bnj110  35191  subfacp1lem1  35604  erdszelem2  35617  dfon2lem3  36208  filnetlem2  36813  ttciunun  36945  taupi  37889  cnviun  44302  coiun1  44304  comptiunov2i  44358  cotrcltrcl  44377  cotrclrcl  44394  ssrab2f  45761  iooinlbub  46143  stirlinglem14  46727  sssalgen  46975  fvmptrabdm  47953  stgr0  48648  unilbss  49515  dfinito4  50198