Theorem mprgbir 3087

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2146  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827

This proof depends on definitions:  df-bi 210  df-ral 3081

This theorem is used by:  ssintub  4929  djussxp  5828  dmiin  5940  dfco2  6253  coiun  6265  tron  6392  onxpdisj  6497  epweon  7799  frrlem6  8323  frrlem7  8324  tfrlem6OLD  8404  oawordeulem  8576  sbthlem1  9120  marypha2lem1  9440  ttrclselem1  9739  rankval4  9897  tcwf  9913  inlresf  10008  inrresf  10010  fin23lem16  10426  fin23lem29  10432  fin23lem30  10433  itunitc  10512  acncc  10531  wfgru  10914  renfdisj  11382  ioomax  13566  iccmax  13567  hashgval2  14535  fsumcom2  15955  fprodcom2  16166  dfphi2  16966  oppccatf  17917  dmcoass  18256  letsr  18782  smndex2dnrinv  19129  efgsf  19958  lssuni  21229  lpival  21663  cnsubdrglem  21739  retos  21939  psr1baslem  22518  istopon  23245  neips  23446  filssufilg  24245  xrhmeo  25282  iscmet3i  25648  ehlbase  25751  ovolge0  25817  unidmvol  25877  resinf1o  26879  divlogrlim  26978  dvloglem  26991  logf1o2  26993  atansssdm  27276  ppiub  27546  bday1  28215  lrrecse  28343  clwwlkn0  30634  sspval  31340  shintcli  31946  lnopco0i  32621  imaelshi  32675  nmopadjlem  32706  nmoptrii  32711  nmopcoi  32712  nmopcoadji  32718  idleop  32748  hmopidmchi  32768  hmopidmpji  32769  djussxp2  33299  xrsclat  33628  rearchi  33963  dmvlsiga  34817  sxbrsigalem0  34959  dya2iocucvr  34972  eulerpartlemgh  35066  bnj110  35544  subfacp1lem1  36068  erdszelem2  36081  dfon2lem3  36677  filnetlem2  37297  ttciunun  37429  taupi  38387  cnviun  44793  coiun1  44795  comptiunov2i  44849  cotrcltrcl  44868  cotrclrcl  44885  ssrab2f  46274  iooinlbub  46655  stirlinglem14  47239  sssalgen  47487  sqrtnpoly  48085  fvmptrabdm  48505  stgr0  49200  unilbss  50071  dfinito4  50778