Theorem mprgbir 3068

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  ∀wral 3061

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

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

This theorem is referenced by:  ss2rabi  4077  ssintub  4966  djussxp  5856  dmiin  5964  dfco2  6265  coiun  6276  tron  6407  onxpdisj  6510  epweon  7795  frrlem6  8316  frrlem7  8317  wfrrelOLD  8354  wfrdmssOLD  8355  tfrlem6  8422  oawordeulem  8592  sbthlem1  9123  marypha2lem1  9475  ttrclselem1  9765  rankval4  9907  tcwf  9923  inlresf  9954  inrresf  9956  fin23lem16  10375  fin23lem29  10381  fin23lem30  10382  itunitc  10461  acncc  10480  wfgru  10856  renfdisj  11321  ioomax  13462  iccmax  13463  hashgval2  14417  fsumcom2  15810  fprodcom2  16020  dfphi2  16811  oppccatf  17771  dmcoass  18111  letsr  18638  smndex2dnrinv  18928  efgsf  19747  lssuni  20937  lpival  21334  cnsubdrglem  21436  retos  21636  psr1baslem  22186  istopon  22918  neips  23121  filssufilg  23919  xrhmeo  24977  iscmet3i  25346  ehlbase  25449  ovolge0  25516  unidmvol  25576  resinf1o  26578  divlogrlim  26677  dvloglem  26690  logf1o2  26692  atansssdm  26976  ppiub  27248  bday1s  27876  lrrecse  27975  clwwlkn0  30047  sspval  30742  shintcli  31348  lnopco0i  32023  imaelshi  32077  nmopadjlem  32108  nmoptrii  32113  nmopcoi  32114  nmopcoadji  32120  idleop  32150  hmopidmchi  32170  hmopidmpji  32171  djussxp2  32658  xrsclat  33013  rearchi  33374  dmvlsiga  34130  sxbrsigalem0  34273  dya2iocucvr  34286  eulerpartlemgh  34380  bnj110  34872  subfacp1lem1  35184  erdszelem2  35197  dfon2lem3  35786  filnetlem2  36380  taupi  37324  cnviun  43663  coiun1  43665  comptiunov2i  43719  cotrcltrcl  43738  cotrclrcl  43755  ssrab2f  45122  iooinlbub  45514  stirlinglem14  46102  sssalgen  46350  fvmptrabdm  47305  stgr0  47927  unilbss  48737