Theorem mprgbir 3084

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2143  ∀wral 3077

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

This theorem depends on definitions:  df-bi 209  df-ral 3078

This theorem is referenced by:  ssintub  4925  djussxp  5818  dmiin  5930  dfco2  6233  coiun  6245  tron  6370  onxpdisj  6474  epweon  7759  frrlem6  8273  frrlem7  8274  tfrlem6OLD  8354  oawordeulem  8524  sbthlem1  9060  marypha2lem1  9382  ttrclselem1  9681  rankval4  9826  tcwf  9842  inlresf  9873  inrresf  9875  fin23lem16  10293  fin23lem29  10299  fin23lem30  10300  itunitc  10379  acncc  10398  wfgru  10775  renfdisj  11243  ioomax  13427  iccmax  13428  hashgval2  14392  fsumcom2  15802  fprodcom2  16015  dfphi2  16810  oppccatf  17761  dmcoass  18100  letsr  18626  smndex2dnrinv  18953  efgsf  19770  lssuni  21007  lpival  21395  cnsubdrglem  21471  retos  21671  psr1baslem  22248  istopon  22973  neips  23174  filssufilg  23972  xrhmeo  25009  iscmet3i  25375  ehlbase  25478  ovolge0  25544  unidmvol  25604  resinf1o  26602  divlogrlim  26701  dvloglem  26714  logf1o2  26716  atansssdm  26999  ppiub  27269  bday1  27908  lrrecse  28036  clwwlkn0  30231  sspval  30927  shintcli  31533  lnopco0i  32208  imaelshi  32262  nmopadjlem  32293  nmoptrii  32298  nmopcoi  32299  nmopcoadji  32305  idleop  32335  hmopidmchi  32355  hmopidmpji  32356  djussxp2  32851  xrsclat  33190  rearchi  33533  dmvlsiga  34427  sxbrsigalem0  34569  dya2iocucvr  34582  eulerpartlemgh  34676  bnj110  35154  subfacp1lem1  35530  erdszelem2  35543  dfon2lem3  36134  filnetlem2  36740  ttciunun  36872  taupi  37816  cnviun  44227  coiun1  44229  comptiunov2i  44283  cotrcltrcl  44302  cotrclrcl  44319  ssrab2f  45696  iooinlbub  46078  stirlinglem14  46662  sssalgen  46910  fvmptrabdm  47888  stgr0  48583  unilbss  49440  dfinito4  50123