Theorem mprgbir 3067

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106  ∀wral 3060

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

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

This theorem is referenced by:  ss2rabi  4039  rabxm  4351  ssintub  4932  djussxp  5806  dmiin  5913  dfco2  6202  coiun  6213  tron  6345  onxpdisj  6448  epweon  7714  frrlem6  8227  frrlem7  8228  wfrrelOLD  8265  wfrdmssOLD  8266  tfrlem6  8333  oawordeulem  8506  sbthlem1  9034  marypha2lem1  9380  ttrclselem1  9670  rankval4  9812  tcwf  9828  inlresf  9859  inrresf  9861  fin23lem16  10280  fin23lem29  10286  fin23lem30  10287  itunitc  10366  acncc  10385  wfgru  10761  renfdisj  11224  ioomax  13349  iccmax  13350  hashgval2  14288  fsumcom2  15670  fprodcom2  15878  dfphi2  16657  oppccatf  17624  dmcoass  17966  letsr  18496  smndex2dnrinv  18739  efgsf  19525  lssuni  20457  lpival  20774  cnsubdrglem  20885  retos  21059  psr1baslem  21593  istopon  22298  neips  22501  filssufilg  23299  xrhmeo  24346  iscmet3i  24713  ehlbase  24816  ovolge0  24882  unidmvol  24942  resinf1o  25929  divlogrlim  26027  dvloglem  26040  logf1o2  26042  atansssdm  26320  ppiub  26589  bday1s  27213  lrrecse  27297  clwwlkn0  29035  sspval  29728  shintcli  30334  lnopco0i  31009  imaelshi  31063  nmopadjlem  31094  nmoptrii  31099  nmopcoi  31100  nmopcoadji  31106  idleop  31136  hmopidmchi  31156  hmopidmpji  31157  djussxp2  31631  xrsclat  31941  rearchi  32209  dmvlsiga  32817  sxbrsigalem0  32960  dya2iocucvr  32973  eulerpartlemgh  33067  bnj110  33559  subfacp1lem1  33860  erdszelem2  33873  dfon2lem3  34446  filnetlem2  34927  taupi  35867  cnviun  42044  coiun1  42046  comptiunov2i  42100  cotrcltrcl  42119  cotrclrcl  42136  ssrab2f  43449  iooinlbub  43859  stirlinglem14  44448  sssalgen  44696  fvmptrabdm  45645  unilbss  47022