Theorem mprgbir 3065

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2105  ∀wral 3058

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

This theorem depends on definitions:  df-bi 207  df-ral 3059

This theorem is referenced by:  ss2rabi  4086  ssintub  4970  djussxp  5858  dmiin  5966  dfco2  6266  coiun  6277  tron  6408  onxpdisj  6511  epweon  7793  frrlem6  8314  frrlem7  8315  wfrrelOLD  8352  wfrdmssOLD  8353  tfrlem6  8420  oawordeulem  8590  sbthlem1  9121  marypha2lem1  9472  ttrclselem1  9762  rankval4  9904  tcwf  9920  inlresf  9951  inrresf  9953  fin23lem16  10372  fin23lem29  10378  fin23lem30  10379  itunitc  10458  acncc  10477  wfgru  10853  renfdisj  11318  ioomax  13458  iccmax  13459  hashgval2  14413  fsumcom2  15806  fprodcom2  16016  dfphi2  16807  oppccatf  17774  dmcoass  18119  letsr  18650  smndex2dnrinv  18940  efgsf  19761  lssuni  20954  lpival  21351  cnsubdrglem  21453  retos  21653  psr1baslem  22201  istopon  22933  neips  23136  filssufilg  23934  xrhmeo  24990  iscmet3i  25359  ehlbase  25462  ovolge0  25529  unidmvol  25589  resinf1o  26592  divlogrlim  26691  dvloglem  26704  logf1o2  26706  atansssdm  26990  ppiub  27262  bday1s  27890  lrrecse  27989  clwwlkn0  30056  sspval  30751  shintcli  31357  lnopco0i  32032  imaelshi  32086  nmopadjlem  32117  nmoptrii  32122  nmopcoi  32123  nmopcoadji  32129  idleop  32159  hmopidmchi  32179  hmopidmpji  32180  djussxp2  32664  xrsclat  32995  rearchi  33353  dmvlsiga  34109  sxbrsigalem0  34252  dya2iocucvr  34265  eulerpartlemgh  34359  bnj110  34850  subfacp1lem1  35163  erdszelem2  35176  dfon2lem3  35766  filnetlem2  36361  taupi  37305  cnviun  43639  coiun1  43641  comptiunov2i  43695  cotrcltrcl  43714  cotrclrcl  43731  ssrab2f  45056  iooinlbub  45453  stirlinglem14  46042  sssalgen  46290  fvmptrabdm  47242  stgr0  47862  unilbss  48665