Theorem mprgbir 3054

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2111  ∀wral 3047

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

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

This theorem is referenced by:  ss2rabi  4023  ssintub  4914  djussxp  5784  dmiin  5892  dfco2  6192  coiun  6204  tron  6329  onxpdisj  6433  epweon  7708  frrlem6  8221  frrlem7  8222  tfrlem6  8301  oawordeulem  8469  sbthlem1  9000  marypha2lem1  9319  ttrclselem1  9615  rankval4  9760  tcwf  9776  inlresf  9807  inrresf  9809  fin23lem16  10226  fin23lem29  10232  fin23lem30  10233  itunitc  10312  acncc  10331  wfgru  10707  renfdisj  11172  ioomax  13322  iccmax  13323  hashgval2  14285  fsumcom2  15681  fprodcom2  15891  dfphi2  16685  oppccatf  17634  dmcoass  17973  letsr  18499  smndex2dnrinv  18823  efgsf  19641  lssuni  20872  lpival  21261  cnsubdrglem  21355  retos  21555  psr1baslem  22097  istopon  22827  neips  23028  filssufilg  23826  xrhmeo  24871  iscmet3i  25239  ehlbase  25342  ovolge0  25409  unidmvol  25469  resinf1o  26472  divlogrlim  26571  dvloglem  26584  logf1o2  26586  atansssdm  26870  ppiub  27142  bday1s  27775  lrrecse  27885  clwwlkn0  30008  sspval  30703  shintcli  31309  lnopco0i  31984  imaelshi  32038  nmopadjlem  32069  nmoptrii  32074  nmopcoi  32075  nmopcoadji  32081  idleop  32111  hmopidmchi  32131  hmopidmpji  32132  djussxp2  32630  xrsclat  32992  rearchi  33311  dmvlsiga  34142  sxbrsigalem0  34284  dya2iocucvr  34297  eulerpartlemgh  34391  bnj110  34870  subfacp1lem1  35223  erdszelem2  35236  dfon2lem3  35827  filnetlem2  36423  taupi  37367  cnviun  43753  coiun1  43755  comptiunov2i  43809  cotrcltrcl  43828  cotrclrcl  43845  ssrab2f  45224  iooinlbub  45611  stirlinglem14  46195  sssalgen  46443  fvmptrabdm  47403  stgr0  48070  unilbss  48928  dfinito4  49612