Theorem mprgbir 3080

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2107  ∀wral 3065

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

This theorem depends on definitions:  df-bi 206  df-ral 3070

This theorem is referenced by:  ss2rabi  4011  rabxm  4321  ssintub  4898  djussxp  5757  dmiin  5865  dfco2  6153  coiun  6164  tron  6293  onxpdisj  6390  epweon  7634  frrlem6  8116  frrlem7  8117  wfrrelOLD  8154  wfrdmssOLD  8155  tfrlem6  8222  oawordeulem  8394  sbthlem1  8879  marypha2lem1  9203  ttrclselem1  9492  rankval4  9634  tcwf  9650  inlresf  9681  inrresf  9683  fin23lem16  10100  fin23lem29  10106  fin23lem30  10107  itunitc  10186  acncc  10205  wfgru  10581  renfdisj  11044  ioomax  13163  iccmax  13164  hashgval2  14102  fsumcom2  15495  fprodcom2  15703  dfphi2  16484  oppccatf  17448  dmcoass  17790  letsr  18320  smndex2dnrinv  18563  efgsf  19344  lssuni  20210  lpival  20525  cnsubdrglem  20658  retos  20832  psr1baslem  21365  istopon  22070  neips  22273  filssufilg  23071  xrhmeo  24118  iscmet3i  24485  ehlbase  24588  ovolge0  24654  unidmvol  24714  resinf1o  25701  divlogrlim  25799  dvloglem  25812  logf1o2  25814  atansssdm  26092  ppiub  26361  clwwlkn0  28401  sspval  29094  shintcli  29700  lnopco0i  30375  imaelshi  30429  nmopadjlem  30460  nmoptrii  30465  nmopcoi  30466  nmopcoadji  30472  idleop  30502  hmopidmchi  30522  hmopidmpji  30523  djussxp2  30994  xrsclat  31298  rearchi  31555  dmvlsiga  32106  sxbrsigalem0  32247  dya2iocucvr  32260  eulerpartlemgh  32354  bnj110  32847  subfacp1lem1  33150  erdszelem2  33163  dfon2lem3  33770  bday1s  34034  lrrecse  34108  filnetlem2  34577  taupi  35503  cnviun  41265  coiun1  41267  comptiunov2i  41321  cotrcltrcl  41340  cotrclrcl  41357  ssrab2f  42673  iooinlbub  43046  stirlinglem14  43635  sssalgen  43881  fvmptrabdm  44796  unilbss  46174