Theorem ralbidv 2544

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
ralbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
ralbidv	|- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem ralbidv

Step	Hyp	Ref	Expression
1		nfv 1577	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	ralbid 2542	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 105   A.wral 2522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  ralbii  2550  2ralbidv  2568  rexralbidv  2570  r19.32vdc  2694  raleqbi1dv  2755  raleqbidv  2759  cbvral2vw  2791  cbvral2v  2793  rspceaimv  2932  rspc2  2935  rspc3v  2940  reu6i  3011  reu7  3015  sbcralt  3122  sbcralg  3124  reu8nf  3127  raaanlem  3618  2ralunsn  3908  elintg  3962  elintrabg  3967  eliin  4001  brralrspcev  4173  bnd2  4291  poeq1  4425  soeq1  4441  frforeq1  4469  frforeq3  4473  frirrg  4476  frind  4478  weeq1  4482  reusv3  4586  ontr2exmid  4652  reg2exmidlema  4661  posng  4827  ralxpf  4906  cnvpom  5310  funcnvuni  5430  fnmptfvd  5787  dff4im  5828  dff13f  5949  eusvobj2  6044  ovanraleqv  6082  ofreq  6279  caofdig  6309  uchoice  6344  suppssrst  6474  suppssrgst  6475  suppofss1dcl  6477  suppofss2dcl  6478  smoeq  6534  recseq  6550  tfr0dm  6566  tfrlemiex  6575  tfr1onlemex  6591  tfr1onlemaccex  6592  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllemex  6604  tfrcllemaccex  6605  tfrcllemres  6606  elixp2  6950  pw2f1odclem  7100  xpf1o  7110  nneneq  7124  ac6sfi  7168  fimax2gtrilemstep  7171  fimax2gtri  7172  elssdc  7175  opabfi  7213  2omap  7282  supeq1  7290  supeq3  7294  supmoti  7297  eqsupti  7300  supubti  7303  suplubti  7304  supisoex  7313  cnvinfex  7322  eqinfti  7324  infvalti  7326  updjud  7386  ctssdclemr  7416  nninff  7426  nninfninc  7427  infnninf  7428  infnninfOLD  7429  nnnninf  7430  nnnninfeq  7432  nnnninfeq2  7433  enomnilem  7442  finomni  7444  exmidomni  7446  fodjuomnilemres  7452  ismkvnex  7459  fodjumkvlemres  7463  enmkvlem  7465  enwomnilem  7473  nninfdcinf  7475  nninfwlporlem  7477  nninfwlpoimlemg  7479  nninfwlpoimlemdc  7481  exmidontriimlem3  7543  exmidontriim  7545  papeq1  7573  papsym  7576  papcotr  7577  tapeq1  7582  netap  7584  exmidapne  7590  cc2lem  7596  cc3  7598  elinp  7805  prloc  7822  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgpr  8013  caucvgprpr  8043  suplocexprlemloc  8052  suplocexpr  8056  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  caucvgsr  8133  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  lbreu  9236  sup3exmid  9248  nnsub  9293  indstr  9943  supinfneg  9945  infsupneg  9946  ublbneg  9963  lbzbi  9966  iccsupr  10318  zsupcllemstep  10611  infssuzex  10615  suprzubdc  10620  nninfdcex  10621  zsupssdc  10622  frecuzrdgsuc  10800  frecuzrdgg  10802  frecuzrdgsuctlem  10809  seq3f1olemstep  10900  seq3f1olemp  10901  seqfeq4g  10917  nn0ltexp2  11096  bccl  11154  hashfibc  11232  wrdind  11439  wrd2ind  11440  cau4  11826  caubnd2  11827  maxleast  11923  rexanre  11930  rexico  11931  fimaxre2  11937  minmax  11940  xrminmax  11975  clim  11991  clim2  11993  clim2c  11994  clim0c  11996  climabs0  12017  cn1lem  12024  sumeq1  12065  prodeq1f  12263  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlemex  12722  bezoutlemeu  12728  dfgcd3  12731  bezout  12732  dfgcd2  12735  nnwodc  12757  uzwodc  12758  nnwofdc  12759  sqrt2irr  12884  reumodprminv  12976  pc2dvds  13053  pcz  13055  prmpwdvds  13078  ballotfileme  13180  ennnfoneleminc  13246  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemnn0  13257  ennnfonelemr  13258  ennnfonelemim  13259  exmidunben  13261  ctinfomlemom  13262  ctinfom  13263  ctinf  13265  ctiunctlemudc  13272  ctiunct  13275  ssomct  13280  infpn2  13291  imasaddfnlemg  13578  mgm1  13633  sgrp1  13674  mhmima  13746  dfgrp2  13782  isgrpinv  13809  grpidinv  13814  dfgrp3mlem  13853  issubg4m  13946  isnsg2  13956  elnmz  13961  ghmrn  14010  ghmnsgima  14021  srgideu  14215  ring1  14302  lringuplu  14441  subrgugrp  14486  isrrg  14509  islssm  14631  islssmg  14632  rnglidlmcl  14754  mplsubgfilemm  14979  mplsubgfilemcl  14980  basgen2  15072  bastop1  15074  iscn  15188  cnpval  15189  iscnp  15190  iscnp3  15194  cnprcl2k  15197  lmbr  15204  lmbr2  15205  lmbrf  15206  cnptoprest  15230  cnptoprest2  15231  cnmpt21  15282  ispsmet  15314  ismet  15335  isxmet  15336  metss  15485  qtopbasss  15512  cncfval  15563  elcncf2  15565  mulc1cncf  15580  cncfmet  15583  dedekindeulemloc  15610  dedekindeulemeu  15613  dedekindeu  15614  suplociccreex  15615  dedekindicclemloc  15619  dedekindicclemeu  15622  dedekindicclemicc  15623  ivthinclemlopn  15627  ivthinclemlr  15628  ivthinclemuopn  15629  ivthinclemur  15630  ivthinclemloc  15632  ivthreinc  15636  dich0  15643  limccl  15650  ellimc3apf  15651  limcdifap  15653  limcmpted  15654  2irrexpqap  15969  perfectlem2  15994  2sqlem6  16119  2sqlem10  16124  wksfval  16443  wlkvtxedg  16484  clwwlkg  16514  depind  16630  bj-charfunbi  16707  bj-omtrans  16852  strcoll2  16879  strcollnfALT  16882  sscoll2  16884  pw1nct  16903  exmidcon  16906  0nninf  16908  nnsf  16909  peano4nninf  16910  nninfalllem1  16912  nninfself  16917  nninfsellemeq  16918  nninfsellemeqinf  16920  isomninnlem  16940  trilpolemlt1  16951  iswomninnlem  16960  iswomni0  16962  ismkvnnlem  16963  cndcap  16970  dceqnconst  16972  dcapnconst  16973  ltlenmkv  16982