Theorem mprgbir 3051

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ∀wral 3044

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 207  df-ral 3045

This theorem is referenced by:  ss2rabi  4028  ssintub  4916  djussxp  5788  dmiin  5895  dfco2  6194  coiun  6205  tron  6330  onxpdisj  6434  epweon  7711  frrlem6  8224  frrlem7  8225  tfrlem6  8304  oawordeulem  8472  sbthlem1  9004  marypha2lem1  9325  ttrclselem1  9621  rankval4  9763  tcwf  9779  inlresf  9810  inrresf  9812  fin23lem16  10229  fin23lem29  10235  fin23lem30  10236  itunitc  10315  acncc  10334  wfgru  10710  renfdisj  11175  ioomax  13325  iccmax  13326  hashgval2  14285  fsumcom2  15681  fprodcom2  15891  dfphi2  16685  oppccatf  17634  dmcoass  17973  letsr  18499  smndex2dnrinv  18789  efgsf  19608  lssuni  20842  lpival  21231  cnsubdrglem  21325  retos  21525  psr1baslem  22067  istopon  22797  neips  22998  filssufilg  23796  xrhmeo  24842  iscmet3i  25210  ehlbase  25313  ovolge0  25380  unidmvol  25440  resinf1o  26443  divlogrlim  26542  dvloglem  26555  logf1o2  26557  atansssdm  26841  ppiub  27113  bday1s  27745  lrrecse  27854  clwwlkn0  29972  sspval  30667  shintcli  31273  lnopco0i  31948  imaelshi  32002  nmopadjlem  32033  nmoptrii  32038  nmopcoi  32039  nmopcoadji  32045  idleop  32075  hmopidmchi  32095  hmopidmpji  32096  djussxp2  32592  xrsclat  32966  rearchi  33284  dmvlsiga  34102  sxbrsigalem0  34245  dya2iocucvr  34258  eulerpartlemgh  34352  bnj110  34831  subfacp1lem1  35162  erdszelem2  35175  dfon2lem3  35769  filnetlem2  36363  taupi  37307  cnviun  43633  coiun1  43635  comptiunov2i  43689  cotrcltrcl  43708  cotrclrcl  43725  ssrab2f  45105  iooinlbub  45492  stirlinglem14  46078  sssalgen  46326  fvmptrabdm  47287  stgr0  47954  unilbss  48812  dfinito4  49496