Theorem ralbidv 2497

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  ralbii  2503  2ralbidv  2521  rexralbidv  2523  r19.32vdc  2646  raleqbi1dv  2705  raleqbidv  2709  cbvral2vw  2740  cbvral2v  2742  rspceaimv  2876  rspc2  2879  rspc3v  2884  reu6i  2955  reu7  2959  sbcralt  3066  sbcralg  3068  raaanlem  3556  2ralunsn  3829  elintg  3883  elintrabg  3888  eliin  3922  brralrspcev  4092  bnd2  4207  poeq1  4335  soeq1  4351  frforeq1  4379  frforeq3  4383  frirrg  4386  frind  4388  weeq1  4392  reusv3  4496  ontr2exmid  4562  reg2exmidlema  4571  posng  4736  ralxpf  4813  cnvpom  5213  funcnvuni  5328  fnmptfvd  5669  dff4im  5711  dff13f  5820  eusvobj2  5911  ovanraleqv  5949  ofreq  6143  caofdig  6173  uchoice  6204  smoeq  6357  recseq  6373  tfr0dm  6389  tfrlemiex  6398  tfr1onlemex  6414  tfr1onlemaccex  6415  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllemex  6427  tfrcllemaccex  6428  tfrcllemres  6429  elixp2  6770  pw2f1odclem  6904  xpf1o  6914  nneneq  6927  ac6sfi  6968  fimax2gtrilemstep  6970  fimax2gtri  6971  opabfi  7008  supeq1  7061  supeq3  7065  supmoti  7068  eqsupti  7071  supubti  7074  suplubti  7075  supisoex  7084  cnvinfex  7093  eqinfti  7095  infvalti  7097  updjud  7157  ctssdclemr  7187  nninff  7197  nninfninc  7198  infnninf  7199  infnninfOLD  7200  nnnninf  7201  nnnninfeq  7203  nnnninfeq2  7204  enomnilem  7213  finomni  7215  exmidomni  7217  fodjuomnilemres  7223  ismkvnex  7230  fodjumkvlemres  7234  enmkvlem  7236  enwomnilem  7244  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemg  7250  nninfwlpoimlemdc  7252  exmidontriimlem3  7306  exmidontriim  7308  tapeq1  7335  netap  7337  exmidapne  7343  cc2lem  7349  cc3  7351  elinp  7558  prloc  7575  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgpr  7766  caucvgprpr  7796  suplocexprlemloc  7805  suplocexpr  7809  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  caucvgsr  7886  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  axcaucvglemcau  7982  axcaucvglemres  7983  axpre-suploclemres  7985  axpre-suploc  7986  lbreu  8989  sup3exmid  9001  nnsub  9046  indstr  9684  supinfneg  9686  infsupneg  9687  ublbneg  9704  lbzbi  9707  iccsupr  10058  zsupcllemstep  10336  infssuzex  10340  suprzubdc  10343  nninfdcex  10344  zsupssdc  10345  frecuzrdgsuc  10523  frecuzrdgg  10525  frecuzrdgsuctlem  10532  seq3f1olemstep  10623  seq3f1olemp  10624  seqfeq4g  10640  nn0ltexp2  10818  bccl  10876  cau4  11298  caubnd2  11299  maxleast  11395  rexanre  11402  rexico  11403  fimaxre2  11409  minmax  11412  xrminmax  11447  clim  11463  clim2  11465  clim2c  11466  clim0c  11468  climabs0  11489  cn1lem  11496  sumeq1  11537  prodeq1f  11734  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlemex  12193  bezoutlemeu  12199  dfgcd3  12202  bezout  12203  dfgcd2  12206  nnwodc  12228  uzwodc  12229  nnwofdc  12230  sqrt2irr  12355  reumodprminv  12447  pc2dvds  12524  pcz  12526  prmpwdvds  12549  ennnfoneleminc  12653  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemnn0  12664  ennnfonelemr  12665  ennnfonelemim  12666  exmidunben  12668  ctinfomlemom  12669  ctinfom  12670  ctinf  12672  ctiunctlemudc  12679  ctiunct  12682  ssomct  12687  infpn2  12698  imasaddfnlemg  13016  mgm1  13072  sgrp1  13113  mhmima  13193  dfgrp2  13229  isgrpinv  13256  grpidinv  13261  dfgrp3mlem  13300  issubg4m  13399  isnsg2  13409  elnmz  13414  ghmrn  13463  ghmnsgima  13474  srgideu  13604  ring1  13691  lringuplu  13828  subrgugrp  13872  isrrg  13895  islssm  13989  islssmg  13990  rnglidlmcl  14112  basgen2  14401  bastop1  14403  iscn  14517  cnpval  14518  iscnp  14519  iscnp3  14523  cnprcl2k  14526  lmbr  14533  lmbr2  14534  lmbrf  14535  cnptoprest  14559  cnptoprest2  14560  cnmpt21  14611  ispsmet  14643  ismet  14664  isxmet  14665  metss  14814  qtopbasss  14841  cncfval  14892  elcncf2  14894  mulc1cncf  14909  cncfmet  14912  dedekindeulemloc  14939  dedekindeulemeu  14942  dedekindeu  14943  suplociccreex  14944  dedekindicclemloc  14948  dedekindicclemeu  14951  dedekindicclemicc  14952  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemloc  14961  ivthreinc  14965  dich0  14972  limccl  14979  ellimc3apf  14980  limcdifap  14982  limcmpted  14983  2irrexpqap  15298  perfectlem2  15320  2sqlem6  15445  2sqlem10  15450  bj-charfunbi  15541  bj-omtrans  15686  strcoll2  15713  strcollnfALT  15716  sscoll2  15718  2omap  15726  pw1nct  15734  0nninf  15735  nnsf  15736  peano4nninf  15737  nninfalllem1  15739  nninfself  15744  nninfsellemeq  15745  nninfsellemeqinf  15747  isomninnlem  15761  trilpolemlt1  15772  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783  cndcap  15790  dceqnconst  15791  dcapnconst  15792  ltlenmkv  15801