Theorem mprgbir 3076

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2110  ∀wral 3061

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

This theorem depends on definitions:  df-bi 210  df-ral 3066

This theorem is referenced by:  ss2rabi  3990  rabxm  4301  ssintub  4877  djussxp  5714  dmiin  5822  dfco2  6109  coiun  6120  tron  6236  onxpdisj  6333  frrlem6  8032  frrlem7  8033  wfrrel  8060  wfrdmss  8061  tfrlem6  8118  oawordeulem  8282  sbthlem1  8756  marypha2lem1  9051  trpredlem1  9332  rankval4  9483  tcwf  9499  inlresf  9530  inrresf  9532  fin23lem16  9949  fin23lem29  9955  fin23lem30  9956  itunitc  10035  acncc  10054  wfgru  10430  renfdisj  10893  ioomax  13010  iccmax  13011  hashgval2  13945  fsumcom2  15338  fprodcom2  15546  dfphi2  16327  oppccatf  17232  dmcoass  17572  letsr  18099  smndex2dnrinv  18342  efgsf  19119  lssuni  19976  lpival  20283  cnsubdrglem  20414  retos  20580  psr1baslem  21106  istopon  21809  neips  22010  filssufilg  22808  xrhmeo  23843  iscmet3i  24209  ehlbase  24312  ovolge0  24378  unidmvol  24438  resinf1o  25425  divlogrlim  25523  dvloglem  25536  logf1o2  25538  atansssdm  25816  ppiub  26085  clwwlkn0  28111  sspval  28804  shintcli  29410  lnopco0i  30085  imaelshi  30139  nmopadjlem  30170  nmoptrii  30175  nmopcoi  30176  nmopcoadji  30182  idleop  30212  hmopidmchi  30232  hmopidmpji  30233  djussxp2  30704  xrsclat  31008  rearchi  31260  dmvlsiga  31809  sxbrsigalem0  31950  dya2iocucvr  31963  eulerpartlemgh  32057  bnj110  32551  subfacp1lem1  32854  erdszelem2  32867  dfon2lem3  33480  bday1s  33762  lrrecse  33836  filnetlem2  34305  taupi  35228  cnviun  40935  coiun1  40937  comptiunov2i  40991  cotrcltrcl  41010  cotrclrcl  41027  ssrab2f  42339  iooinlbub  42714  stirlinglem14  43303  sssalgen  43549  fvmptrabdm  44457  unilbss  45836