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  2915  rspc2  2918  rspc3v  2923  reu6i  2994  reu7  2998  sbcralt  3105  sbcralg  3107  reu8nf  3110  raaanlem  3596  2ralunsn  3877  elintg  3931  elintrabg  3936  eliin  3970  brralrspcev  4142  bnd2  4257  poeq1  4390  soeq1  4406  frforeq1  4434  frforeq3  4438  frirrg  4441  frind  4443  weeq1  4447  reusv3  4551  ontr2exmid  4617  reg2exmidlema  4626  posng  4791  ralxpf  4868  cnvpom  5271  funcnvuni  5390  fnmptfvd  5739  dff4im  5781  dff13f  5894  eusvobj2  5987  ovanraleqv  6025  ofreq  6222  caofdig  6252  uchoice  6283  smoeq  6436  recseq  6452  tfr0dm  6468  tfrlemiex  6477  tfr1onlemex  6493  tfr1onlemaccex  6494  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllemex  6506  tfrcllemaccex  6507  tfrcllemres  6508  elixp2  6849  pw2f1odclem  6995  xpf1o  7005  nneneq  7018  ac6sfi  7060  fimax2gtrilemstep  7062  fimax2gtri  7063  opabfi  7100  supeq1  7153  supeq3  7157  supmoti  7160  eqsupti  7163  supubti  7166  suplubti  7167  supisoex  7176  cnvinfex  7185  eqinfti  7187  infvalti  7189  updjud  7249  ctssdclemr  7279  nninff  7289  nninfninc  7290  infnninf  7291  infnninfOLD  7292  nnnninf  7293  nnnninfeq  7295  nnnninfeq2  7296  enomnilem  7305  finomni  7307  exmidomni  7309  fodjuomnilemres  7315  ismkvnex  7322  fodjumkvlemres  7326  enmkvlem  7328  enwomnilem  7336  nninfdcinf  7338  nninfwlporlem  7340  nninfwlpoimlemg  7342  nninfwlpoimlemdc  7344  exmidontriimlem3  7405  exmidontriim  7407  tapeq1  7438  netap  7440  exmidapne  7446  cc2lem  7452  cc3  7454  elinp  7661  prloc  7678  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  caucvgpr  7869  caucvgprpr  7899  suplocexprlemloc  7908  suplocexpr  7912  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  caucvgsr  7989  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  axcaucvglemcau  8085  axcaucvglemres  8086  axpre-suploclemres  8088  axpre-suploc  8089  lbreu  9092  sup3exmid  9104  nnsub  9149  indstr  9788  supinfneg  9790  infsupneg  9791  ublbneg  9808  lbzbi  9811  iccsupr  10162  zsupcllemstep  10449  infssuzex  10453  suprzubdc  10456  nninfdcex  10457  zsupssdc  10458  frecuzrdgsuc  10636  frecuzrdgg  10638  frecuzrdgsuctlem  10645  seq3f1olemstep  10736  seq3f1olemp  10737  seqfeq4g  10753  nn0ltexp2  10931  bccl  10989  wrdind  11254  wrd2ind  11255  cau4  11627  caubnd2  11628  maxleast  11724  rexanre  11731  rexico  11732  fimaxre2  11738  minmax  11741  xrminmax  11776  clim  11792  clim2  11794  clim2c  11795  clim0c  11797  climabs0  11818  cn1lem  11825  sumeq1  11866  prodeq1f  12063  bezoutlemstep  12518  bezoutlemmain  12519  bezoutlemex  12522  bezoutlemeu  12528  dfgcd3  12531  bezout  12532  dfgcd2  12535  nnwodc  12557  uzwodc  12558  nnwofdc  12559  sqrt2irr  12684  reumodprminv  12776  pc2dvds  12853  pcz  12855  prmpwdvds  12878  ennnfoneleminc  12982  ennnfonelemex  12985  ennnfonelemhom  12986  ennnfonelemnn0  12993  ennnfonelemr  12994  ennnfonelemim  12995  exmidunben  12997  ctinfomlemom  12998  ctinfom  12999  ctinf  13001  ctiunctlemudc  13008  ctiunct  13011  ssomct  13016  infpn2  13027  imasaddfnlemg  13347  mgm1  13403  sgrp1  13444  mhmima  13524  dfgrp2  13560  isgrpinv  13587  grpidinv  13592  dfgrp3mlem  13631  issubg4m  13730  isnsg2  13740  elnmz  13745  ghmrn  13794  ghmnsgima  13805  srgideu  13935  ring1  14022  lringuplu  14160  subrgugrp  14204  isrrg  14227  islssm  14321  islssmg  14322  rnglidlmcl  14444  mplsubgfilemm  14662  mplsubgfilemcl  14663  basgen2  14755  bastop1  14757  iscn  14871  cnpval  14872  iscnp  14873  iscnp3  14877  cnprcl2k  14880  lmbr  14887  lmbr2  14888  lmbrf  14889  cnptoprest  14913  cnptoprest2  14914  cnmpt21  14965  ispsmet  14997  ismet  15018  isxmet  15019  metss  15168  qtopbasss  15195  cncfval  15246  elcncf2  15248  mulc1cncf  15263  cncfmet  15266  dedekindeulemloc  15293  dedekindeulemeu  15296  dedekindeu  15297  suplociccreex  15298  dedekindicclemloc  15302  dedekindicclemeu  15305  dedekindicclemicc  15306  ivthinclemlopn  15310  ivthinclemlr  15311  ivthinclemuopn  15312  ivthinclemur  15313  ivthinclemloc  15315  ivthreinc  15319  dich0  15326  limccl  15333  ellimc3apf  15334  limcdifap  15336  limcmpted  15337  2irrexpqap  15652  perfectlem2  15674  2sqlem6  15799  2sqlem10  15804  wksfval  16035  wlkvtxedg  16074  bj-charfunbi  16174  bj-omtrans  16319  strcoll2  16346  strcollnfALT  16349  sscoll2  16351  2omap  16359  pw1nct  16369  0nninf  16370  nnsf  16371  peano4nninf  16372  nninfalllem1  16374  nninfself  16379  nninfsellemeq  16380  nninfsellemeqinf  16382  isomninnlem  16398  trilpolemlt1  16409  iswomninnlem  16417  iswomni0  16419  ismkvnnlem  16420  cndcap  16427  dceqnconst  16428  dcapnconst  16429  ltlenmkv  16438