Theorem mprgbir 3078

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2108  ∀wral 3063

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

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

This theorem is referenced by:  ss2rabi  4006  rabxm  4317  ssintub  4894  djussxp  5743  dmiin  5851  dfco2  6138  coiun  6149  tron  6274  onxpdisj  6371  frrlem6  8078  frrlem7  8079  wfrrelOLD  8116  wfrdmssOLD  8117  tfrlem6  8184  oawordeulem  8347  sbthlem1  8823  marypha2lem1  9124  trpredlem1  9405  rankval4  9556  tcwf  9572  inlresf  9603  inrresf  9605  fin23lem16  10022  fin23lem29  10028  fin23lem30  10029  itunitc  10108  acncc  10127  wfgru  10503  renfdisj  10966  ioomax  13083  iccmax  13084  hashgval2  14021  fsumcom2  15414  fprodcom2  15622  dfphi2  16403  oppccatf  17356  dmcoass  17697  letsr  18226  smndex2dnrinv  18469  efgsf  19250  lssuni  20116  lpival  20429  cnsubdrglem  20561  retos  20735  psr1baslem  21266  istopon  21969  neips  22172  filssufilg  22970  xrhmeo  24015  iscmet3i  24381  ehlbase  24484  ovolge0  24550  unidmvol  24610  resinf1o  25597  divlogrlim  25695  dvloglem  25708  logf1o2  25710  atansssdm  25988  ppiub  26257  clwwlkn0  28293  sspval  28986  shintcli  29592  lnopco0i  30267  imaelshi  30321  nmopadjlem  30352  nmoptrii  30357  nmopcoi  30358  nmopcoadji  30364  idleop  30394  hmopidmchi  30414  hmopidmpji  30415  djussxp2  30886  xrsclat  31191  rearchi  31448  dmvlsiga  31997  sxbrsigalem0  32138  dya2iocucvr  32151  eulerpartlemgh  32245  bnj110  32738  subfacp1lem1  33041  erdszelem2  33054  dfon2lem3  33667  ttrclselem1  33711  bday1s  33952  lrrecse  34026  filnetlem2  34495  taupi  35421  cnviun  41147  coiun1  41149  comptiunov2i  41203  cotrcltrcl  41222  cotrclrcl  41239  ssrab2f  42555  iooinlbub  42929  stirlinglem14  43518  sssalgen  43764  fvmptrabdm  44672  unilbss  46051