Theorem mprgbir 3084

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ral 3078

This theorem is used by:  ssintub  4926  djussxp  5823  dmiin  5935  dfco2  6246  coiun  6258  tron  6385  onxpdisj  6490  epweon  7789  frrlem6  8309  frrlem7  8310  tfrlem6OLD  8390  oawordeulem  8562  sbthlem1  9106  marypha2lem1  9427  ttrclselem1  9726  rankval4  9884  tcwf  9900  inlresf  9995  inrresf  9997  fin23lem16  10413  fin23lem29  10419  fin23lem30  10420  itunitc  10499  acncc  10518  wfgru  10901  renfdisj  11369  ioomax  13553  iccmax  13554  hashgval2  14522  fsumcom2  15940  fprodcom2  16151  dfphi2  16951  oppccatf  17902  dmcoass  18241  letsr  18767  smndex2dnrinv  19114  efgsf  19943  lssuni  21214  lpival  21648  cnsubdrglem  21724  retos  21924  psr1baslem  22503  istopon  23230  neips  23431  filssufilg  24230  xrhmeo  25267  iscmet3i  25633  ehlbase  25736  ovolge0  25802  unidmvol  25862  resinf1o  26864  divlogrlim  26963  dvloglem  26976  logf1o2  26978  atansssdm  27261  ppiub  27531  bday1  28200  lrrecse  28328  clwwlkn0  30619  sspval  31325  shintcli  31931  lnopco0i  32606  imaelshi  32660  nmopadjlem  32691  nmoptrii  32696  nmopcoi  32697  nmopcoadji  32703  idleop  32733  hmopidmchi  32753  hmopidmpji  32754  djussxp2  33242  xrsclat  33572  rearchi  33907  dmvlsiga  34761  sxbrsigalem0  34903  dya2iocucvr  34916  eulerpartlemgh  35010  bnj110  35488  subfacp1lem1  35944  erdszelem2  35957  dfon2lem3  36547  filnetlem2  37167  ttciunun  37299  taupi  38244  cnviun  44649  coiun1  44651  comptiunov2i  44705  cotrcltrcl  44724  cotrclrcl  44741  ssrab2f  46131  iooinlbub  46512  stirlinglem14  47096  sssalgen  47344  sqrtnpoly  47942  fvmptrabdm  48362  stgr0  49057  unilbss  49927  dfinito4  50608