Theorem mprgbir 3083

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

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

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

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

This theorem is used by:  ssintub  4926  djussxp  5825  dmiin  5937  dfco2  6241  coiun  6253  tron  6380  onxpdisj  6485  epweon  7775  frrlem6  8291  frrlem7  8292  tfrlem6OLD  8372  oawordeulem  8544  sbthlem1  9088  marypha2lem1  9408  ttrclselem1  9707  rankval4  9852  tcwf  9868  inlresf  9922  inrresf  9924  fin23lem16  10340  fin23lem29  10346  fin23lem30  10347  itunitc  10426  acncc  10445  wfgru  10828  renfdisj  11296  ioomax  13478  iccmax  13479  hashgval2  14445  fsumcom2  15863  fprodcom2  16074  dfphi2  16868  oppccatf  17819  dmcoass  18158  letsr  18684  smndex2dnrinv  19030  efgsf  19859  lssuni  21126  lpival  21558  cnsubdrglem  21634  retos  21834  psr1baslem  22413  istopon  23140  neips  23341  filssufilg  24140  xrhmeo  25177  iscmet3i  25543  ehlbase  25646  ovolge0  25712  unidmvol  25772  resinf1o  26776  divlogrlim  26875  dvloglem  26888  logf1o2  26890  atansssdm  27173  ppiub  27443  bday1  28082  lrrecse  28210  clwwlkn0  30501  sspval  31207  shintcli  31813  lnopco0i  32488  imaelshi  32542  nmopadjlem  32573  nmoptrii  32578  nmopcoi  32579  nmopcoadji  32585  idleop  32615  hmopidmchi  32635  hmopidmpji  32636  djussxp2  33124  xrsclat  33454  rearchi  33789  dmvlsiga  34642  sxbrsigalem0  34785  dya2iocucvr  34798  eulerpartlemgh  34892  bnj110  35370  subfacp1lem1  35761  erdszelem2  35774  dfon2lem3  36365  filnetlem2  37001  ttciunun  37133  taupi  38078  cnviun  44493  coiun1  44495  comptiunov2i  44549  cotrcltrcl  44568  cotrclrcl  44585  ssrab2f  45952  iooinlbub  46334  stirlinglem14  46918  sssalgen  47166  sqrtnpoly  47764  fvmptrabdm  48184  stgr0  48879  unilbss  49749  dfinito4  50430