Theorem ralbidv 2533

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  ralbii  2539  2ralbidv  2557  rexralbidv  2559  r19.32vdc  2683  raleqbi1dv  2743  raleqbidv  2747  cbvral2vw  2779  cbvral2v  2781  rspceaimv  2919  rspc2  2922  rspc3v  2927  reu6i  2998  reu7  3002  sbcralt  3109  sbcralg  3111  reu8nf  3114  raaanlem  3601  2ralunsn  3887  elintg  3941  elintrabg  3946  eliin  3980  brralrspcev  4152  bnd2  4269  poeq1  4402  soeq1  4418  frforeq1  4446  frforeq3  4450  frirrg  4453  frind  4455  weeq1  4459  reusv3  4563  ontr2exmid  4629  reg2exmidlema  4638  posng  4804  ralxpf  4882  cnvpom  5286  funcnvuni  5406  fnmptfvd  5760  dff4im  5801  dff13f  5921  eusvobj2  6014  ovanraleqv  6052  ofreq  6248  caofdig  6278  uchoice  6309  suppssrst  6439  suppssrgst  6440  suppofss1dcl  6442  suppofss2dcl  6443  smoeq  6499  recseq  6515  tfr0dm  6531  tfrlemiex  6540  tfr1onlemex  6556  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemex  6569  tfrcllemaccex  6570  tfrcllemres  6571  elixp2  6914  pw2f1odclem  7063  xpf1o  7073  nneneq  7086  ac6sfi  7130  fimax2gtrilemstep  7133  fimax2gtri  7134  elssdc  7137  opabfi  7175  supeq1  7245  supeq3  7249  supmoti  7252  eqsupti  7255  supubti  7258  suplubti  7259  supisoex  7268  cnvinfex  7277  eqinfti  7279  infvalti  7281  updjud  7341  ctssdclemr  7371  nninff  7381  nninfninc  7382  infnninf  7383  infnninfOLD  7384  nnnninf  7385  nnnninfeq  7387  nnnninfeq2  7388  enomnilem  7397  finomni  7399  exmidomni  7401  fodjuomnilemres  7407  ismkvnex  7414  fodjumkvlemres  7418  enmkvlem  7420  enwomnilem  7428  nninfdcinf  7430  nninfwlporlem  7432  nninfwlpoimlemg  7434  nninfwlpoimlemdc  7436  exmidontriimlem3  7498  exmidontriim  7500  tapeq1  7531  netap  7533  exmidapne  7539  cc2lem  7545  cc3  7547  elinp  7754  prloc  7771  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  caucvgpr  7962  caucvgprpr  7992  suplocexprlemloc  8001  suplocexpr  8005  caucvgsrlemgt1  8075  caucvgsrlemoffres  8080  caucvgsr  8082  suplocsrlemb  8086  suplocsrlempr  8087  suplocsrlem  8088  axcaucvglemcau  8178  axcaucvglemres  8179  axpre-suploclemres  8181  axpre-suploc  8182  lbreu  9184  sup3exmid  9196  nnsub  9241  indstr  9888  supinfneg  9890  infsupneg  9891  ublbneg  9908  lbzbi  9911  iccsupr  10262  zsupcllemstep  10552  infssuzex  10556  suprzubdc  10559  nninfdcex  10560  zsupssdc  10561  frecuzrdgsuc  10739  frecuzrdgg  10741  frecuzrdgsuctlem  10748  seq3f1olemstep  10839  seq3f1olemp  10840  seqfeq4g  10856  nn0ltexp2  11034  bccl  11092  wrdind  11369  wrd2ind  11370  cau4  11756  caubnd2  11757  maxleast  11853  rexanre  11860  rexico  11861  fimaxre2  11867  minmax  11870  xrminmax  11905  clim  11921  clim2  11923  clim2c  11924  clim0c  11926  climabs0  11947  cn1lem  11954  sumeq1  11995  prodeq1f  12193  bezoutlemstep  12648  bezoutlemmain  12649  bezoutlemex  12652  bezoutlemeu  12658  dfgcd3  12661  bezout  12662  dfgcd2  12665  nnwodc  12687  uzwodc  12688  nnwofdc  12689  sqrt2irr  12814  reumodprminv  12906  pc2dvds  12983  pcz  12985  prmpwdvds  13008  ennnfoneleminc  13112  ennnfonelemex  13115  ennnfonelemhom  13116  ennnfonelemnn0  13123  ennnfonelemr  13124  ennnfonelemim  13125  exmidunben  13127  ctinfomlemom  13128  ctinfom  13129  ctinf  13131  ctiunctlemudc  13138  ctiunct  13141  ssomct  13146  infpn2  13157  imasaddfnlemg  13477  mgm1  13533  sgrp1  13574  mhmima  13654  dfgrp2  13690  isgrpinv  13717  grpidinv  13722  dfgrp3mlem  13761  issubg4m  13860  isnsg2  13870  elnmz  13875  ghmrn  13924  ghmnsgima  13935  srgideu  14066  ring1  14153  lringuplu  14291  subrgugrp  14335  isrrg  14358  islssm  14453  islssmg  14454  rnglidlmcl  14576  mplsubgfilemm  14799  mplsubgfilemcl  14800  basgen2  14892  bastop1  14894  iscn  15008  cnpval  15009  iscnp  15010  iscnp3  15014  cnprcl2k  15017  lmbr  15024  lmbr2  15025  lmbrf  15026  cnptoprest  15050  cnptoprest2  15051  cnmpt21  15102  ispsmet  15134  ismet  15155  isxmet  15156  metss  15305  qtopbasss  15332  cncfval  15383  elcncf2  15385  mulc1cncf  15400  cncfmet  15403  dedekindeulemloc  15430  dedekindeulemeu  15433  dedekindeu  15434  suplociccreex  15435  dedekindicclemloc  15439  dedekindicclemeu  15442  dedekindicclemicc  15443  ivthinclemlopn  15447  ivthinclemlr  15448  ivthinclemuopn  15449  ivthinclemur  15450  ivthinclemloc  15452  ivthreinc  15456  dich0  15463  limccl  15470  ellimc3apf  15471  limcdifap  15473  limcmpted  15474  2irrexpqap  15789  perfectlem2  15814  2sqlem6  15939  2sqlem10  15944  wksfval  16263  wlkvtxedg  16304  clwwlkg  16334  depind  16450  bj-charfunbi  16527  bj-omtrans  16672  strcoll2  16699  strcollnfALT  16702  sscoll2  16704  2omap  16715  pw1nct  16725  exmidcon  16728  0nninf  16730  nnsf  16731  peano4nninf  16732  nninfalllem1  16734  nninfself  16739  nninfsellemeq  16740  nninfsellemeqinf  16742  isomninnlem  16762  trilpolemlt1  16773  iswomninnlem  16782  iswomni0  16784  ismkvnnlem  16785  cndcap  16792  dceqnconst  16793  dcapnconst  16794  ltlenmkv  16803