Theorem mprgbir 3086

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2143  ∀wral 3079

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

This theorem depends on definitions:  df-bi 210  df-ral 3080

This theorem is referenced by:  ssintub  4931  djussxp  5831  dmiin  5943  dfco2  6246  coiun  6258  tron  6383  onxpdisj  6488  epweon  7770  frrlem6  8284  frrlem7  8285  tfrlem6OLD  8365  oawordeulem  8535  sbthlem1  9071  marypha2lem1  9391  ttrclselem1  9690  rankval4  9835  tcwf  9851  inlresf  9896  inrresf  9898  fin23lem16  10314  fin23lem29  10320  fin23lem30  10321  itunitc  10400  acncc  10419  wfgru  10796  renfdisj  11264  ioomax  13444  iccmax  13445  hashgval2  14410  fsumcom2  15821  fprodcom2  16034  dfphi2  16828  oppccatf  17779  dmcoass  18118  letsr  18644  smndex2dnrinv  18972  efgsf  19794  lssuni  21060  lpival  21492  cnsubdrglem  21568  retos  21768  psr1baslem  22345  istopon  23069  neips  23270  filssufilg  24068  xrhmeo  25105  iscmet3i  25471  ehlbase  25574  ovolge0  25640  unidmvol  25700  resinf1o  26701  divlogrlim  26800  dvloglem  26813  logf1o2  26815  atansssdm  27098  ppiub  27368  bday1  28007  lrrecse  28135  clwwlkn0  30379  sspval  31075  shintcli  31681  lnopco0i  32356  imaelshi  32410  nmopadjlem  32441  nmoptrii  32446  nmopcoi  32447  nmopcoadji  32453  idleop  32483  hmopidmchi  32503  hmopidmpji  32504  djussxp2  32993  xrsclat  33331  rearchi  33666  dmvlsiga  34519  sxbrsigalem0  34661  dya2iocucvr  34674  eulerpartlemgh  34768  bnj110  35246  subfacp1lem1  35671  erdszelem2  35684  dfon2lem3  36275  filnetlem2  36910  ttciunun  37042  taupi  37987  cnviun  44396  coiun1  44398  comptiunov2i  44452  cotrcltrcl  44471  cotrclrcl  44488  ssrab2f  45855  iooinlbub  46237  stirlinglem14  46821  sssalgen  47069  fvmptrabdm  48050  stgr0  48745  unilbss  49616  dfinito4  50299