Theorem ralbidv 2530

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 1574	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	ralbid 2528	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralbii  2536  2ralbidv  2554  rexralbidv  2556  r19.32vdc  2680  raleqbi1dv  2740  raleqbidv  2744  cbvral2vw  2776  cbvral2v  2778  rspceaimv  2916  rspc2  2919  rspc3v  2924  reu6i  2995  reu7  2999  sbcralt  3106  sbcralg  3108  reu8nf  3111  raaanlem  3597  2ralunsn  3880  elintg  3934  elintrabg  3939  eliin  3973  brralrspcev  4145  bnd2  4261  poeq1  4394  soeq1  4410  frforeq1  4438  frforeq3  4442  frirrg  4445  frind  4447  weeq1  4451  reusv3  4555  ontr2exmid  4621  reg2exmidlema  4630  posng  4796  ralxpf  4874  cnvpom  5277  funcnvuni  5396  fnmptfvd  5747  dff4im  5789  dff13f  5906  eusvobj2  5999  ovanraleqv  6037  ofreq  6234  caofdig  6264  uchoice  6295  smoeq  6451  recseq  6467  tfr0dm  6483  tfrlemiex  6492  tfr1onlemex  6508  tfr1onlemaccex  6509  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllemex  6521  tfrcllemaccex  6522  tfrcllemres  6523  elixp2  6866  pw2f1odclem  7015  xpf1o  7025  nneneq  7038  ac6sfi  7080  fimax2gtrilemstep  7083  fimax2gtri  7084  elssdc  7087  opabfi  7123  supeq1  7176  supeq3  7180  supmoti  7183  eqsupti  7186  supubti  7189  suplubti  7190  supisoex  7199  cnvinfex  7208  eqinfti  7210  infvalti  7212  updjud  7272  ctssdclemr  7302  nninff  7312  nninfninc  7313  infnninf  7314  infnninfOLD  7315  nnnninf  7316  nnnninfeq  7318  nnnninfeq2  7319  enomnilem  7328  finomni  7330  exmidomni  7332  fodjuomnilemres  7338  ismkvnex  7345  fodjumkvlemres  7349  enmkvlem  7351  enwomnilem  7359  nninfdcinf  7361  nninfwlporlem  7363  nninfwlpoimlemg  7365  nninfwlpoimlemdc  7367  exmidontriimlem3  7428  exmidontriim  7430  tapeq1  7461  netap  7463  exmidapne  7469  cc2lem  7475  cc3  7477  elinp  7684  prloc  7701  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgpr  7892  caucvgprpr  7922  suplocexprlemloc  7931  suplocexpr  7935  caucvgsrlemgt1  8005  caucvgsrlemoffres  8010  caucvgsr  8012  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  axcaucvglemcau  8108  axcaucvglemres  8109  axpre-suploclemres  8111  axpre-suploc  8112  lbreu  9115  sup3exmid  9127  nnsub  9172  indstr  9817  supinfneg  9819  infsupneg  9820  ublbneg  9837  lbzbi  9840  iccsupr  10191  zsupcllemstep  10479  infssuzex  10483  suprzubdc  10486  nninfdcex  10487  zsupssdc  10488  frecuzrdgsuc  10666  frecuzrdgg  10668  frecuzrdgsuctlem  10675  seq3f1olemstep  10766  seq3f1olemp  10767  seqfeq4g  10783  nn0ltexp2  10961  bccl  11019  wrdind  11293  wrd2ind  11294  cau4  11667  caubnd2  11668  maxleast  11764  rexanre  11771  rexico  11772  fimaxre2  11778  minmax  11781  xrminmax  11816  clim  11832  clim2  11834  clim2c  11835  clim0c  11837  climabs0  11858  cn1lem  11865  sumeq1  11906  prodeq1f  12103  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlemex  12562  bezoutlemeu  12568  dfgcd3  12571  bezout  12572  dfgcd2  12575  nnwodc  12597  uzwodc  12598  nnwofdc  12599  sqrt2irr  12724  reumodprminv  12816  pc2dvds  12893  pcz  12895  prmpwdvds  12918  ennnfoneleminc  13022  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemnn0  13033  ennnfonelemr  13034  ennnfonelemim  13035  exmidunben  13037  ctinfomlemom  13038  ctinfom  13039  ctinf  13041  ctiunctlemudc  13048  ctiunct  13051  ssomct  13056  infpn2  13067  imasaddfnlemg  13387  mgm1  13443  sgrp1  13484  mhmima  13564  dfgrp2  13600  isgrpinv  13627  grpidinv  13632  dfgrp3mlem  13671  issubg4m  13770  isnsg2  13780  elnmz  13785  ghmrn  13834  ghmnsgima  13845  srgideu  13975  ring1  14062  lringuplu  14200  subrgugrp  14244  isrrg  14267  islssm  14361  islssmg  14362  rnglidlmcl  14484  mplsubgfilemm  14702  mplsubgfilemcl  14703  basgen2  14795  bastop1  14797  iscn  14911  cnpval  14912  iscnp  14913  iscnp3  14917  cnprcl2k  14920  lmbr  14927  lmbr2  14928  lmbrf  14929  cnptoprest  14953  cnptoprest2  14954  cnmpt21  15005  ispsmet  15037  ismet  15058  isxmet  15059  metss  15208  qtopbasss  15235  cncfval  15286  elcncf2  15288  mulc1cncf  15303  cncfmet  15306  dedekindeulemloc  15333  dedekindeulemeu  15336  dedekindeu  15337  suplociccreex  15338  dedekindicclemloc  15342  dedekindicclemeu  15345  dedekindicclemicc  15346  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemloc  15355  ivthreinc  15359  dich0  15366  limccl  15373  ellimc3apf  15374  limcdifap  15376  limcmpted  15377  2irrexpqap  15692  perfectlem2  15714  2sqlem6  15839  2sqlem10  15844  wksfval  16119  wlkvtxedg  16160  clwwlkg  16188  bj-charfunbi  16342  bj-omtrans  16487  strcoll2  16514  strcollnfALT  16517  sscoll2  16519  2omap  16530  pw1nct  16540  0nninf  16542  nnsf  16543  peano4nninf  16544  nninfalllem1  16546  nninfself  16551  nninfsellemeq  16552  nninfsellemeqinf  16554  isomninnlem  16570  trilpolemlt1  16581  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592  cndcap  16599  dceqnconst  16600  dcapnconst  16601  ltlenmkv  16610