Theorem ralbidv 2490

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473

This theorem is referenced by:  ralbii  2496  2ralbidv  2514  rexralbidv  2516  r19.32vdc  2639  raleqbi1dv  2694  raleqbidv  2698  cbvral2vw  2729  cbvral2v  2731  rspceaimv  2864  rspc2  2867  rspc3v  2872  reu6i  2943  reu7  2947  sbcralt  3054  sbcralg  3056  raaanlem  3543  2ralunsn  3813  elintg  3867  elintrabg  3872  eliin  3906  brralrspcev  4076  bnd2  4191  poeq1  4317  soeq1  4333  frforeq1  4361  frforeq3  4365  frirrg  4368  frind  4370  weeq1  4374  reusv3  4478  ontr2exmid  4542  reg2exmidlema  4551  posng  4716  ralxpf  4791  cnvpom  5189  funcnvuni  5304  fnmptfvd  5641  dff4im  5683  dff13f  5792  eusvobj2  5882  ovanraleqv  5920  ofreq  6110  smoeq  6315  recseq  6331  tfr0dm  6347  tfrlemiex  6356  tfr1onlemex  6372  tfr1onlemaccex  6373  tfrcllemsucaccv  6379  tfrcllembxssdm  6381  tfrcllemex  6385  tfrcllemaccex  6386  tfrcllemres  6387  elixp2  6728  pw2f1odclem  6862  xpf1o  6872  nneneq  6885  ac6sfi  6926  fimax2gtrilemstep  6928  fimax2gtri  6929  supeq1  7015  supeq3  7019  supmoti  7022  eqsupti  7025  supubti  7028  suplubti  7029  supisoex  7038  cnvinfex  7047  eqinfti  7049  infvalti  7051  updjud  7111  ctssdclemr  7141  nninff  7151  infnninf  7152  infnninfOLD  7153  nnnninf  7154  nnnninfeq  7156  nnnninfeq2  7157  enomnilem  7166  finomni  7168  exmidomni  7170  fodjuomnilemres  7176  ismkvnex  7183  fodjumkvlemres  7187  enmkvlem  7189  enwomnilem  7197  nninfdcinf  7199  nninfwlporlem  7201  nninfwlpoimlemg  7203  nninfwlpoimlemdc  7205  exmidontriimlem3  7252  exmidontriim  7254  tapeq1  7281  netap  7283  exmidapne  7289  cc2lem  7295  cc3  7297  elinp  7503  prloc  7520  cauappcvgprlemladdru  7685  cauappcvgprlemladdrl  7686  caucvgpr  7711  caucvgprpr  7741  suplocexprlemloc  7750  suplocexpr  7754  caucvgsrlemgt1  7824  caucvgsrlemoffres  7829  caucvgsr  7831  suplocsrlemb  7835  suplocsrlempr  7836  suplocsrlem  7837  axcaucvglemcau  7927  axcaucvglemres  7928  axpre-suploclemres  7930  axpre-suploc  7931  lbreu  8932  sup3exmid  8944  nnsub  8988  indstr  9623  supinfneg  9625  infsupneg  9626  ublbneg  9643  lbzbi  9646  iccsupr  9996  frecuzrdgsuc  10445  frecuzrdgg  10447  frecuzrdgsuctlem  10454  seq3f1olemstep  10532  seq3f1olemp  10533  nn0ltexp2  10721  bccl  10779  cau4  11157  caubnd2  11158  maxleast  11254  rexanre  11261  rexico  11262  fimaxre2  11267  minmax  11270  xrminmax  11305  clim  11321  clim2  11323  clim2c  11324  clim0c  11326  climabs0  11347  cn1lem  11354  sumeq1  11395  prodeq1f  11592  zsupcllemstep  11978  infssuzex  11982  suprzubdc  11985  nninfdcex  11986  zsupssdc  11987  bezoutlemstep  12030  bezoutlemmain  12031  bezoutlemex  12034  bezoutlemeu  12040  dfgcd3  12043  bezout  12044  dfgcd2  12047  nnwodc  12069  uzwodc  12070  nnwofdc  12071  sqrt2irr  12194  reumodprminv  12285  pc2dvds  12362  pcz  12364  prmpwdvds  12387  ennnfoneleminc  12462  ennnfonelemex  12465  ennnfonelemhom  12466  ennnfonelemnn0  12473  ennnfonelemr  12474  ennnfonelemim  12475  exmidunben  12477  ctinfomlemom  12478  ctinfom  12479  ctinf  12481  ctiunctlemudc  12488  ctiunct  12491  ssomct  12496  infpn2  12507  imasaddfnlemg  12791  mgm1  12846  sgrp1  12874  mhmima  12943  dfgrp2  12971  isgrpinv  12998  grpidinv  13003  dfgrp3mlem  13042  issubg4m  13132  isnsg2  13142  elnmz  13147  ghmrn  13196  ghmnsgima  13207  srgideu  13326  ring1  13411  lringuplu  13543  subrgugrp  13587  islssm  13673  islssmg  13674  rnglidlmcl  13796  basgen2  14041  bastop1  14043  iscn  14157  cnpval  14158  iscnp  14159  iscnp3  14163  cnprcl2k  14166  lmbr  14173  lmbr2  14174  lmbrf  14175  cnptoprest  14199  cnptoprest2  14200  cnmpt21  14251  ispsmet  14283  ismet  14304  isxmet  14305  metss  14454  qtopbasss  14481  cncfval  14519  elcncf2  14521  mulc1cncf  14536  cncfmet  14539  dedekindeulemloc  14557  dedekindeulemeu  14560  dedekindeu  14561  suplociccreex  14562  dedekindicclemloc  14566  dedekindicclemeu  14569  dedekindicclemicc  14570  ivthinclemlopn  14574  ivthinclemlr  14575  ivthinclemuopn  14576  ivthinclemur  14577  ivthinclemloc  14579  limccl  14588  ellimc3apf  14589  limcdifap  14591  limcmpted  14592  2irrexpqap  14856  2sqlem6  14928  2sqlem10  14933  bj-charfunbi  15024  bj-omtrans  15169  strcoll2  15196  strcollnfALT  15199  sscoll2  15201  pw1nct  15214  0nninf  15215  nnsf  15216  peano4nninf  15217  nninfalllem1  15219  nninfself  15224  nninfsellemeq  15225  nninfsellemeqinf  15227  isomninnlem  15240  trilpolemlt1  15251  iswomninnlem  15259  iswomni0  15261  ismkvnnlem  15262  cndcap  15269  dceqnconst  15270  dcapnconst  15271  ltlenmkv  15280