Theorem mprgbir 3119

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

Syntax hints:   → wi 4   ↔ wb 207   ∈ wcel 2080  ∀wral 3104

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

This theorem depends on definitions:  df-bi 208  df-ral 3109

This theorem is referenced by:  ss2rabi  3976  rabxm  4262  ssintub  4802  djussxp  5605  dmiin  5710  dfco2  5976  coiun  5987  tron  6092  onxpdisj  6188  wfrrel  7815  wfrdmss  7816  tfrlem6  7873  oawordeulem  8033  sbthlem1  8477  marypha2lem1  8748  rankval4  9145  tcwf  9161  inlresf  9192  inrresf  9194  fin23lem16  9606  fin23lem29  9612  fin23lem30  9613  itunitc  9692  acncc  9711  wfgru  10087  renfdisj  10550  ioomax  12661  iccmax  12662  hashgval2  13587  fsumcom2  14962  fprodcom2  15171  dfphi2  15940  dmcoass  17155  letsr  17666  efgsf  18582  lssuni  19401  lpival  19707  psr1baslem  20036  cnsubdrglem  20278  retos  20444  istopon  21204  neips  21405  filssufilg  22203  xrhmeo  23233  iscmet3i  23598  ehlbase  23701  ovolge0  23765  unidmvol  23825  resinf1o  24801  divlogrlim  24899  dvloglem  24912  logf1o2  24914  atansssdm  25192  ppiub  25462  clwwlkn0  27488  sspval  28183  shintcli  28789  lnopco0i  29464  imaelshi  29518  nmopadjlem  29549  nmoptrii  29554  nmopcoi  29555  nmopcoadji  29561  idleop  29591  hmopidmchi  29611  hmopidmpji  29612  xrsclat  30333  rearchi  30561  dmvlsiga  30997  sxbrsigalem0  31138  dya2iocucvr  31151  eulerpartlemgh  31245  bnj110  31738  subfacp1lem1  32028  erdszelem2  32041  dfon2lem3  32632  trpredlem1  32669  frrlem6  32731  frrlem7  32732  filnetlem2  33330  taupi  34148  cnviun  39493  coiun1  39495  comptiunov2i  39549  cotrcltrcl  39568  cotrclrcl  39585  ssrab2f  40936  iooinlbub  41331  stirlinglem14  41928  sssalgen  42174  fvmptrabdm  43022