Theorem mprgbir 3081

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2110  ∀wral 3066

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

This theorem depends on definitions:  df-bi 206  df-ral 3071

This theorem is referenced by:  ss2rabi  4015  rabxm  4326  ssintub  4903  djussxp  5753  dmiin  5861  dfco2  6148  coiun  6159  tron  6288  onxpdisj  6385  epweon  7619  frrlem6  8098  frrlem7  8099  wfrrelOLD  8136  wfrdmssOLD  8137  tfrlem6  8204  oawordeulem  8370  sbthlem1  8852  marypha2lem1  9172  ttrclselem1  9461  trpredlem1  9474  rankval4  9626  tcwf  9642  inlresf  9673  inrresf  9675  fin23lem16  10092  fin23lem29  10098  fin23lem30  10099  itunitc  10178  acncc  10197  wfgru  10573  renfdisj  11036  ioomax  13153  iccmax  13154  hashgval2  14091  fsumcom2  15484  fprodcom2  15692  dfphi2  16473  oppccatf  17437  dmcoass  17779  letsr  18309  smndex2dnrinv  18552  efgsf  19333  lssuni  20199  lpival  20514  cnsubdrglem  20647  retos  20821  psr1baslem  21354  istopon  22059  neips  22262  filssufilg  23060  xrhmeo  24107  iscmet3i  24474  ehlbase  24577  ovolge0  24643  unidmvol  24703  resinf1o  25690  divlogrlim  25788  dvloglem  25801  logf1o2  25803  atansssdm  26081  ppiub  26350  clwwlkn0  28388  sspval  29081  shintcli  29687  lnopco0i  30362  imaelshi  30416  nmopadjlem  30447  nmoptrii  30452  nmopcoi  30453  nmopcoadji  30459  idleop  30489  hmopidmchi  30509  hmopidmpji  30510  djussxp2  30981  xrsclat  31285  rearchi  31542  dmvlsiga  32093  sxbrsigalem0  32234  dya2iocucvr  32247  eulerpartlemgh  32341  bnj110  32834  subfacp1lem1  33137  erdszelem2  33150  dfon2lem3  33757  bday1s  34021  lrrecse  34095  filnetlem2  34564  taupi  35490  cnviun  41228  coiun1  41230  comptiunov2i  41284  cotrcltrcl  41303  cotrclrcl  41320  ssrab2f  42636  iooinlbub  43010  stirlinglem14  43599  sssalgen  43845  fvmptrabdm  44753  unilbss  46132