Theorem ralbidv 2466

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

Syntax hints:   -> wi 4   <-> wb 104   A.wral 2444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449

This theorem is referenced by:  ralbii  2472  2ralbidv  2490  rexralbidv  2492  r19.32vdc  2615  raleqbi1dv  2669  raleqbidv  2673  cbvral2vw  2703  cbvral2v  2705  rspceaimv  2838  rspc2  2841  rspc3v  2846  reu6i  2917  reu7  2921  sbcralt  3027  sbcralg  3029  raaanlem  3514  2ralunsn  3778  elintg  3832  elintrabg  3837  eliin  3871  brralrspcev  4040  bnd2  4152  poeq1  4277  soeq1  4293  frforeq1  4321  frforeq3  4325  frirrg  4328  frind  4330  weeq1  4334  reusv3  4438  ontr2exmid  4502  reg2exmidlema  4511  posng  4676  ralxpf  4750  cnvpom  5146  funcnvuni  5257  dff4im  5631  dff13f  5738  eusvobj2  5828  ovanraleqv  5866  ofreq  6053  smoeq  6258  recseq  6274  tfr0dm  6290  tfrlemiex  6299  tfr1onlemex  6315  tfr1onlemaccex  6316  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllemex  6328  tfrcllemaccex  6329  tfrcllemres  6330  elixp2  6668  xpf1o  6810  nneneq  6823  ac6sfi  6864  fimax2gtrilemstep  6866  fimax2gtri  6867  supeq1  6951  supeq3  6955  supmoti  6958  eqsupti  6961  supubti  6964  suplubti  6965  supisoex  6974  cnvinfex  6983  eqinfti  6985  infvalti  6987  updjud  7047  ctssdclemr  7077  nninff  7087  infnninf  7088  infnninfOLD  7089  nnnninf  7090  nnnninfeq  7092  nnnninfeq2  7093  enomnilem  7102  finomni  7104  exmidomni  7106  fodjuomnilemres  7112  ismkvnex  7119  fodjumkvlemres  7123  enmkvlem  7125  enwomnilem  7133  exmidontriimlem3  7179  exmidontriim  7181  cc2lem  7207  cc3  7209  elinp  7415  prloc  7432  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  caucvgpr  7623  caucvgprpr  7653  suplocexprlemloc  7662  suplocexpr  7666  caucvgsrlemgt1  7736  caucvgsrlemoffres  7741  caucvgsr  7743  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  axcaucvglemcau  7839  axcaucvglemres  7840  axpre-suploclemres  7842  axpre-suploc  7843  lbreu  8840  sup3exmid  8852  nnsub  8896  indstr  9531  supinfneg  9533  infsupneg  9534  ublbneg  9551  lbzbi  9554  iccsupr  9902  frecuzrdgsuc  10349  frecuzrdgg  10351  frecuzrdgsuctlem  10358  seq3f1olemstep  10436  seq3f1olemp  10437  nn0ltexp2  10623  bccl  10680  cau4  11058  caubnd2  11059  maxleast  11155  rexanre  11162  rexico  11163  fimaxre2  11168  minmax  11171  xrminmax  11206  clim  11222  clim2  11224  clim2c  11225  clim0c  11227  climabs0  11248  cn1lem  11255  sumeq1  11296  prodeq1f  11493  zsupcllemstep  11878  infssuzex  11882  suprzubdc  11885  nninfdcex  11886  zsupssdc  11887  bezoutlemstep  11930  bezoutlemmain  11931  bezoutlemex  11934  bezoutlemeu  11940  dfgcd3  11943  bezout  11944  dfgcd2  11947  nnwodc  11969  uzwodc  11970  nnwofdc  11971  sqrt2irr  12094  reumodprminv  12185  pc2dvds  12261  pcz  12263  prmpwdvds  12285  ennnfoneleminc  12344  ennnfonelemex  12347  ennnfonelemhom  12348  ennnfonelemnn0  12355  ennnfonelemr  12356  ennnfonelemim  12357  exmidunben  12359  ctinfomlemom  12360  ctinfom  12361  ctinf  12363  ctiunctlemudc  12370  ctiunct  12373  ssomct  12378  infpn2  12389  mgm1  12601  basgen2  12721  bastop1  12723  iscn  12837  cnpval  12838  iscnp  12839  iscnp3  12843  cnprcl2k  12846  lmbr  12853  lmbr2  12854  lmbrf  12855  cnptoprest  12879  cnptoprest2  12880  cnmpt21  12931  ispsmet  12963  ismet  12984  isxmet  12985  metss  13134  qtopbasss  13161  cncfval  13199  elcncf2  13201  mulc1cncf  13216  cncfmet  13219  dedekindeulemloc  13237  dedekindeulemeu  13240  dedekindeu  13241  suplociccreex  13242  dedekindicclemloc  13246  dedekindicclemeu  13249  dedekindicclemicc  13250  ivthinclemlopn  13254  ivthinclemlr  13255  ivthinclemuopn  13256  ivthinclemur  13257  ivthinclemloc  13259  limccl  13268  ellimc3apf  13269  limcdifap  13271  limcmpted  13272  2irrexpqap  13536  2sqlem6  13596  2sqlem10  13601  bj-charfunbi  13693  bj-omtrans  13838  strcoll2  13865  strcollnfALT  13868  sscoll2  13870  pw1nct  13883  0nninf  13884  nnsf  13885  peano4nninf  13886  nninfalllem1  13888  nninfself  13893  nninfsellemeq  13894  nninfsellemeqinf  13896  isomninnlem  13909  trilpolemlt1  13920  iswomninnlem  13928  iswomni0  13930  ismkvnnlem  13931  dceqnconst  13938  dcapnconst  13939