Theorem ralbidv 2391

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-ral 2375

This theorem is referenced by:  ralbii  2395  2ralbidv  2413  rexralbidv  2415  r19.32vdc  2530  raleqbi1dv  2584  raleqbidv  2588  cbvral2v  2612  rspceaimv  2743  rspc2  2746  rspc3v  2751  reu6i  2820  reu7  2824  sbcralt  2929  sbcralg  2931  raaanlem  3407  2ralunsn  3664  elintg  3718  elintrabg  3723  eliin  3757  bnd2  4029  poeq1  4150  soeq1  4166  frforeq1  4194  frforeq3  4198  frirrg  4201  frind  4203  weeq1  4207  reusv3  4310  ontr2exmid  4369  reg2exmidlema  4378  posng  4539  ralxpf  4613  cnvpom  5007  funcnvuni  5117  dff4im  5484  dff13f  5587  eusvobj2  5676  ovanraleqv  5714  ofreq  5897  smoeq  6093  recseq  6109  tfr0dm  6125  tfrlemiex  6134  tfr1onlemex  6150  tfr1onlemaccex  6151  tfrcllemsucaccv  6157  tfrcllembxssdm  6159  tfrcllemex  6163  tfrcllemaccex  6164  tfrcllemres  6165  elixp2  6499  xpf1o  6640  nneneq  6653  ac6sfi  6694  fimax2gtrilemstep  6696  fimax2gtri  6697  supeq1  6761  supeq3  6765  supmoti  6768  eqsupti  6771  supubti  6774  suplubti  6775  supisoex  6784  cnvinfex  6793  eqinfti  6795  infvalti  6797  updjud  6853  enomnilem  6881  finomni  6883  exmidomni  6885  fodjuomnilemres  6891  infnninf  6893  nnnninf  6894  fodjumkvlemres  6902  elinp  7130  prloc  7147  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  caucvgpr  7338  caucvgprpr  7368  caucvgsrlemgt1  7437  caucvgsrlemoffres  7442  caucvgsr  7444  axcaucvglemcau  7530  axcaucvglemres  7531  lbreu  8503  sup3exmid  8515  nnsub  8559  indstr  9180  supinfneg  9182  infsupneg  9183  ublbneg  9197  lbzbi  9200  iccsupr  9532  frecuzrdgsuc  9970  frecuzrdgg  9972  frecuzrdgsuctlem  9979  seq3f1olemstep  10067  seq3f1olemp  10068  bccl  10306  cau4  10680  caubnd2  10681  maxleast  10777  rexanre  10784  rexico  10785  fimaxre2  10789  minmax  10792  xrminmax  10824  clim  10840  clim2  10842  clim2c  10843  clim0c  10845  climabs0  10866  cn1lem  10872  sumeq1  10913  zsupcllemstep  11383  infssuzex  11387  bezoutlemstep  11428  bezoutlemmain  11429  bezoutlemex  11432  bezoutlemeu  11438  dfgcd3  11441  bezout  11442  dfgcd2  11445  sqrt2irr  11583  basgen2  11948  bastop1  11950  iscn  12063  cnpval  12064  iscnp  12065  iscnp3  12069  cnprcl2k  12072  lmbr  12079  lmbr2  12080  lmbrf  12081  cnptoprest  12105  cnptoprest2  12106  ispsmet  12124  ismet  12145  isxmet  12146  metss  12295  qtopbasss  12315  cncfval  12340  elcncf2  12342  mulc1cncf  12357  bj-omtrans  12563  0nninf  12602  nninff  12603  nnsf  12604  peano4nninf  12605  nninfalllemn  12607  nninfalllem1  12608  nninfself  12614  nninfsellemeq  12615  nninfsellemeqinf  12617