Theorem mprgbir 3059

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∀wral 3052

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

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

This theorem is referenced by:  ssintub  4923  djussxp  5802  dmiin  5910  dfco2  6211  coiun  6223  tron  6348  onxpdisj  6452  epweon  7730  frrlem6  8243  frrlem7  8244  tfrlem6  8323  oawordeulem  8491  sbthlem1  9027  marypha2lem1  9350  ttrclselem1  9646  rankval4  9791  tcwf  9807  inlresf  9838  inrresf  9840  fin23lem16  10257  fin23lem29  10263  fin23lem30  10264  itunitc  10343  acncc  10362  wfgru  10739  renfdisj  11204  ioomax  13350  iccmax  13351  hashgval2  14313  fsumcom2  15709  fprodcom2  15919  dfphi2  16713  oppccatf  17663  dmcoass  18002  letsr  18528  smndex2dnrinv  18855  efgsf  19673  lssuni  20905  lpival  21294  cnsubdrglem  21388  retos  21588  psr1baslem  22140  istopon  22871  neips  23072  filssufilg  23870  xrhmeo  24915  iscmet3i  25283  ehlbase  25386  ovolge0  25453  unidmvol  25513  resinf1o  26516  divlogrlim  26615  dvloglem  26628  logf1o2  26630  atansssdm  26914  ppiub  27186  bday1  27825  lrrecse  27953  clwwlkn0  30119  sspval  30815  shintcli  31421  lnopco0i  32096  imaelshi  32150  nmopadjlem  32181  nmoptrii  32186  nmopcoi  32187  nmopcoadji  32193  idleop  32223  hmopidmchi  32243  hmopidmpji  32244  djussxp2  32742  xrsclat  33108  rearchi  33443  dmvlsiga  34311  sxbrsigalem0  34453  dya2iocucvr  34466  eulerpartlemgh  34560  bnj110  35038  subfacp1lem1  35399  erdszelem2  35412  dfon2lem3  36003  filnetlem2  36599  taupi  37582  cnviun  44010  coiun1  44012  comptiunov2i  44066  cotrcltrcl  44085  cotrclrcl  44102  ssrab2f  45480  iooinlbub  45865  stirlinglem14  46449  sssalgen  46697  fvmptrabdm  47657  stgr0  48324  unilbss  49181  dfinito4  49864