Theorem mprgbir 3153

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2114  ∀wral 3138

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 209  df-ral 3143

This theorem is referenced by:  ss2rabi  4053  rabxm  4340  ssintub  4894  djussxp  5716  dmiin  5825  dfco2  6098  coiun  6109  tron  6214  onxpdisj  6310  wfrrel  7960  wfrdmss  7961  tfrlem6  8018  oawordeulem  8180  sbthlem1  8627  marypha2lem1  8899  rankval4  9296  tcwf  9312  inlresf  9343  inrresf  9345  fin23lem16  9757  fin23lem29  9763  fin23lem30  9764  itunitc  9843  acncc  9862  wfgru  10238  renfdisj  10701  ioomax  12812  iccmax  12813  hashgval2  13740  fsumcom2  15129  fprodcom2  15338  dfphi2  16111  dmcoass  17326  letsr  17837  smndex2dnrinv  18080  efgsf  18855  lssuni  19711  lpival  20018  psr1baslem  20353  cnsubdrglem  20596  retos  20762  istopon  21520  neips  21721  filssufilg  22519  xrhmeo  23550  iscmet3i  23915  ehlbase  24018  ovolge0  24082  unidmvol  24142  resinf1o  25120  divlogrlim  25218  dvloglem  25231  logf1o2  25233  atansssdm  25511  ppiub  25780  clwwlkn0  27806  sspval  28500  shintcli  29106  lnopco0i  29781  imaelshi  29835  nmopadjlem  29866  nmoptrii  29871  nmopcoi  29872  nmopcoadji  29878  idleop  29908  hmopidmchi  29928  hmopidmpji  29929  xrsclat  30667  rearchi  30915  dmvlsiga  31388  sxbrsigalem0  31529  dya2iocucvr  31542  eulerpartlemgh  31636  bnj110  32130  subfacp1lem1  32426  erdszelem2  32439  dfon2lem3  33030  trpredlem1  33066  frrlem6  33128  frrlem7  33129  filnetlem2  33727  taupi  34607  cnviun  40044  coiun1  40046  comptiunov2i  40100  cotrcltrcl  40119  cotrclrcl  40136  ssrab2f  41432  iooinlbub  41825  stirlinglem14  42421  sssalgen  42667  fvmptrabdm  43541