Theorem ralbidv 2532

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

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  ralbii  2538  2ralbidv  2556  rexralbidv  2558  r19.32vdc  2682  raleqbi1dv  2742  raleqbidv  2746  cbvral2vw  2778  cbvral2v  2780  rspceaimv  2918  rspc2  2921  rspc3v  2926  reu6i  2997  reu7  3001  sbcralt  3108  sbcralg  3110  reu8nf  3113  raaanlem  3599  2ralunsn  3882  elintg  3936  elintrabg  3941  eliin  3975  brralrspcev  4147  bnd2  4263  poeq1  4396  soeq1  4412  frforeq1  4440  frforeq3  4444  frirrg  4447  frind  4449  weeq1  4453  reusv3  4557  ontr2exmid  4623  reg2exmidlema  4632  posng  4798  ralxpf  4876  cnvpom  5279  funcnvuni  5399  fnmptfvd  5751  dff4im  5793  dff13f  5911  eusvobj2  6004  ovanraleqv  6042  ofreq  6239  caofdig  6269  uchoice  6300  smoeq  6456  recseq  6472  tfr0dm  6488  tfrlemiex  6497  tfr1onlemex  6513  tfr1onlemaccex  6514  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemex  6526  tfrcllemaccex  6527  tfrcllemres  6528  elixp2  6871  pw2f1odclem  7020  xpf1o  7030  nneneq  7043  ac6sfi  7087  fimax2gtrilemstep  7090  fimax2gtri  7091  elssdc  7094  opabfi  7132  supeq1  7185  supeq3  7189  supmoti  7192  eqsupti  7195  supubti  7198  suplubti  7199  supisoex  7208  cnvinfex  7217  eqinfti  7219  infvalti  7221  updjud  7281  ctssdclemr  7311  nninff  7321  nninfninc  7322  infnninf  7323  infnninfOLD  7324  nnnninf  7325  nnnninfeq  7327  nnnninfeq2  7328  enomnilem  7337  finomni  7339  exmidomni  7341  fodjuomnilemres  7347  ismkvnex  7354  fodjumkvlemres  7358  enmkvlem  7360  enwomnilem  7368  nninfdcinf  7370  nninfwlporlem  7372  nninfwlpoimlemg  7374  nninfwlpoimlemdc  7376  exmidontriimlem3  7438  exmidontriim  7440  tapeq1  7471  netap  7473  exmidapne  7479  cc2lem  7485  cc3  7487  elinp  7694  prloc  7711  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgpr  7902  caucvgprpr  7932  suplocexprlemloc  7941  suplocexpr  7945  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  caucvgsr  8022  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  lbreu  9125  sup3exmid  9137  nnsub  9182  indstr  9827  supinfneg  9829  infsupneg  9830  ublbneg  9847  lbzbi  9850  iccsupr  10201  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  nninfdcex  10498  zsupssdc  10499  frecuzrdgsuc  10677  frecuzrdgg  10679  frecuzrdgsuctlem  10686  seq3f1olemstep  10777  seq3f1olemp  10778  seqfeq4g  10794  nn0ltexp2  10972  bccl  11030  wrdind  11307  wrd2ind  11308  cau4  11694  caubnd2  11695  maxleast  11791  rexanre  11798  rexico  11799  fimaxre2  11805  minmax  11808  xrminmax  11843  clim  11859  clim2  11861  clim2c  11862  clim0c  11864  climabs0  11885  cn1lem  11892  sumeq1  11933  prodeq1f  12131  bezoutlemstep  12586  bezoutlemmain  12587  bezoutlemex  12590  bezoutlemeu  12596  dfgcd3  12599  bezout  12600  dfgcd2  12603  nnwodc  12625  uzwodc  12626  nnwofdc  12627  sqrt2irr  12752  reumodprminv  12844  pc2dvds  12921  pcz  12923  prmpwdvds  12946  ennnfoneleminc  13050  ennnfonelemex  13053  ennnfonelemhom  13054  ennnfonelemnn0  13061  ennnfonelemr  13062  ennnfonelemim  13063  exmidunben  13065  ctinfomlemom  13066  ctinfom  13067  ctinf  13069  ctiunctlemudc  13076  ctiunct  13079  ssomct  13084  infpn2  13095  imasaddfnlemg  13415  mgm1  13471  sgrp1  13512  mhmima  13592  dfgrp2  13628  isgrpinv  13655  grpidinv  13660  dfgrp3mlem  13699  issubg4m  13798  isnsg2  13808  elnmz  13813  ghmrn  13862  ghmnsgima  13873  srgideu  14004  ring1  14091  lringuplu  14229  subrgugrp  14273  isrrg  14296  islssm  14390  islssmg  14391  rnglidlmcl  14513  mplsubgfilemm  14731  mplsubgfilemcl  14732  basgen2  14824  bastop1  14826  iscn  14940  cnpval  14941  iscnp  14942  iscnp3  14946  cnprcl2k  14949  lmbr  14956  lmbr2  14957  lmbrf  14958  cnptoprest  14982  cnptoprest2  14983  cnmpt21  15034  ispsmet  15066  ismet  15087  isxmet  15088  metss  15237  qtopbasss  15264  cncfval  15315  elcncf2  15317  mulc1cncf  15332  cncfmet  15335  dedekindeulemloc  15362  dedekindeulemeu  15365  dedekindeu  15366  suplociccreex  15367  dedekindicclemloc  15371  dedekindicclemeu  15374  dedekindicclemicc  15375  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemloc  15384  ivthreinc  15388  dich0  15395  limccl  15402  ellimc3apf  15403  limcdifap  15405  limcmpted  15406  2irrexpqap  15721  perfectlem2  15743  2sqlem6  15868  2sqlem10  15873  wksfval  16192  wlkvtxedg  16233  clwwlkg  16263  depind  16379  bj-charfunbi  16457  bj-omtrans  16602  strcoll2  16629  strcollnfALT  16632  sscoll2  16634  2omap  16645  pw1nct  16655  0nninf  16657  nnsf  16658  peano4nninf  16659  nninfalllem1  16661  nninfself  16666  nninfsellemeq  16667  nninfsellemeqinf  16669  isomninnlem  16685  trilpolemlt1  16696  iswomninnlem  16705  iswomni0  16707  ismkvnnlem  16708  cndcap  16715  dceqnconst  16716  dcapnconst  16717  ltlenmkv  16726