Theorem mprgbir 3068

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

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

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 3062

This theorem is referenced by:  ss2rabi  4074  rabxm  4386  ssintub  4970  djussxp  5845  dmiin  5952  dfco2  6244  coiun  6255  tron  6387  onxpdisj  6490  epweon  7764  frrlem6  8278  frrlem7  8279  wfrrelOLD  8316  wfrdmssOLD  8317  tfrlem6  8384  oawordeulem  8556  sbthlem1  9085  marypha2lem1  9432  ttrclselem1  9722  rankval4  9864  tcwf  9880  inlresf  9911  inrresf  9913  fin23lem16  10332  fin23lem29  10338  fin23lem30  10339  itunitc  10418  acncc  10437  wfgru  10813  renfdisj  11276  ioomax  13401  iccmax  13402  hashgval2  14340  fsumcom2  15722  fprodcom2  15930  dfphi2  16709  oppccatf  17676  dmcoass  18018  letsr  18548  smndex2dnrinv  18798  efgsf  19599  lssuni  20555  lpival  20889  cnsubdrglem  21002  retos  21177  psr1baslem  21715  istopon  22421  neips  22624  filssufilg  23422  xrhmeo  24469  iscmet3i  24836  ehlbase  24939  ovolge0  25005  unidmvol  25065  resinf1o  26052  divlogrlim  26150  dvloglem  26163  logf1o2  26165  atansssdm  26445  ppiub  26714  bday1s  27340  lrrecse  27435  clwwlkn0  29319  sspval  30014  shintcli  30620  lnopco0i  31295  imaelshi  31349  nmopadjlem  31380  nmoptrii  31385  nmopcoi  31386  nmopcoadji  31392  idleop  31422  hmopidmchi  31442  hmopidmpji  31443  djussxp2  31911  xrsclat  32219  rearchi  32502  dmvlsiga  33196  sxbrsigalem0  33339  dya2iocucvr  33352  eulerpartlemgh  33446  bnj110  33938  subfacp1lem1  34239  erdszelem2  34252  dfon2lem3  34826  filnetlem2  35350  taupi  36290  cnviun  42483  coiun1  42485  comptiunov2i  42539  cotrcltrcl  42558  cotrclrcl  42575  ssrab2f  43888  iooinlbub  44293  stirlinglem14  44882  sssalgen  45130  fvmptrabdm  46080  unilbss  47580