Theorem mprgbir 3060

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2098  ∀wral 3053

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

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

This theorem is referenced by:  ss2rabi  4067  rabxm  4379  ssintub  4961  djussxp  5836  dmiin  5943  dfco2  6235  coiun  6246  tron  6378  onxpdisj  6481  epweon  7756  frrlem6  8272  frrlem7  8273  wfrrelOLD  8310  wfrdmssOLD  8311  tfrlem6  8378  oawordeulem  8550  sbthlem1  9080  marypha2lem1  9427  ttrclselem1  9717  rankval4  9859  tcwf  9875  inlresf  9906  inrresf  9908  fin23lem16  10327  fin23lem29  10333  fin23lem30  10334  itunitc  10413  acncc  10432  wfgru  10808  renfdisj  11272  ioomax  13397  iccmax  13398  hashgval2  14336  fsumcom2  15718  fprodcom2  15926  dfphi2  16708  oppccatf  17675  dmcoass  18020  letsr  18550  smndex2dnrinv  18832  efgsf  19641  lssuni  20778  lpival  21169  cnsubdrglem  21282  retos  21481  psr1baslem  22029  istopon  22738  neips  22941  filssufilg  23739  xrhmeo  24795  iscmet3i  25164  ehlbase  25267  ovolge0  25334  unidmvol  25394  resinf1o  26389  divlogrlim  26488  dvloglem  26501  logf1o2  26503  atansssdm  26784  ppiub  27056  bday1s  27683  lrrecse  27778  clwwlkn0  29753  sspval  30448  shintcli  31054  lnopco0i  31729  imaelshi  31783  nmopadjlem  31814  nmoptrii  31819  nmopcoi  31820  nmopcoadji  31826  idleop  31856  hmopidmchi  31876  hmopidmpji  31877  djussxp2  32345  xrsclat  32651  rearchi  32930  dmvlsiga  33619  sxbrsigalem0  33762  dya2iocucvr  33775  eulerpartlemgh  33869  bnj110  34360  subfacp1lem1  34661  erdszelem2  34674  dfon2lem3  35253  filnetlem2  35755  taupi  36695  cnviun  42915  coiun1  42917  comptiunov2i  42971  cotrcltrcl  42990  cotrclrcl  43007  ssrab2f  44319  iooinlbub  44724  stirlinglem14  45313  sssalgen  45561  fvmptrabdm  46511  unilbss  47714