Theorem ralbidv 2470

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

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

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  ralbii  2476  2ralbidv  2494  rexralbidv  2496  r19.32vdc  2619  raleqbi1dv  2673  raleqbidv  2677  cbvral2vw  2707  cbvral2v  2709  rspceaimv  2842  rspc2  2845  rspc3v  2850  reu6i  2921  reu7  2925  sbcralt  3031  sbcralg  3033  raaanlem  3519  2ralunsn  3783  elintg  3837  elintrabg  3842  eliin  3876  brralrspcev  4045  bnd2  4157  poeq1  4282  soeq1  4298  frforeq1  4326  frforeq3  4330  frirrg  4333  frind  4335  weeq1  4339  reusv3  4443  ontr2exmid  4507  reg2exmidlema  4516  posng  4681  ralxpf  4755  cnvpom  5151  funcnvuni  5265  fnmptfvd  5598  dff4im  5640  dff13f  5747  eusvobj2  5837  ovanraleqv  5875  ofreq  6062  smoeq  6267  recseq  6283  tfr0dm  6299  tfrlemiex  6308  tfr1onlemex  6324  tfr1onlemaccex  6325  tfrcllemsucaccv  6331  tfrcllembxssdm  6333  tfrcllemex  6337  tfrcllemaccex  6338  tfrcllemres  6339  elixp2  6678  xpf1o  6820  nneneq  6833  ac6sfi  6874  fimax2gtrilemstep  6876  fimax2gtri  6877  supeq1  6961  supeq3  6965  supmoti  6968  eqsupti  6971  supubti  6974  suplubti  6975  supisoex  6984  cnvinfex  6993  eqinfti  6995  infvalti  6997  updjud  7057  ctssdclemr  7087  nninff  7097  infnninf  7098  infnninfOLD  7099  nnnninf  7100  nnnninfeq  7102  nnnninfeq2  7103  enomnilem  7112  finomni  7114  exmidomni  7116  fodjuomnilemres  7122  ismkvnex  7129  fodjumkvlemres  7133  enmkvlem  7135  enwomnilem  7143  nninfdcinf  7145  nninfwlporlem  7147  exmidontriimlem3  7193  exmidontriim  7195  cc2lem  7221  cc3  7223  elinp  7429  prloc  7446  cauappcvgprlemladdru  7611  cauappcvgprlemladdrl  7612  caucvgpr  7637  caucvgprpr  7667  suplocexprlemloc  7676  suplocexpr  7680  caucvgsrlemgt1  7750  caucvgsrlemoffres  7755  caucvgsr  7757  suplocsrlemb  7761  suplocsrlempr  7762  suplocsrlem  7763  axcaucvglemcau  7853  axcaucvglemres  7854  axpre-suploclemres  7856  axpre-suploc  7857  lbreu  8854  sup3exmid  8866  nnsub  8910  indstr  9545  supinfneg  9547  infsupneg  9548  ublbneg  9565  lbzbi  9568  iccsupr  9916  frecuzrdgsuc  10363  frecuzrdgg  10365  frecuzrdgsuctlem  10372  seq3f1olemstep  10450  seq3f1olemp  10451  nn0ltexp2  10637  bccl  10694  cau4  11073  caubnd2  11074  maxleast  11170  rexanre  11177  rexico  11178  fimaxre2  11183  minmax  11186  xrminmax  11221  clim  11237  clim2  11239  clim2c  11240  clim0c  11242  climabs0  11263  cn1lem  11270  sumeq1  11311  prodeq1f  11508  zsupcllemstep  11893  infssuzex  11897  suprzubdc  11900  nninfdcex  11901  zsupssdc  11902  bezoutlemstep  11945  bezoutlemmain  11946  bezoutlemex  11949  bezoutlemeu  11955  dfgcd3  11958  bezout  11959  dfgcd2  11962  nnwodc  11984  uzwodc  11985  nnwofdc  11986  sqrt2irr  12109  reumodprminv  12200  pc2dvds  12276  pcz  12278  prmpwdvds  12300  ennnfoneleminc  12359  ennnfonelemex  12362  ennnfonelemhom  12363  ennnfonelemnn0  12370  ennnfonelemr  12371  ennnfonelemim  12372  exmidunben  12374  ctinfomlemom  12375  ctinfom  12376  ctinf  12378  ctiunctlemudc  12385  ctiunct  12388  ssomct  12393  infpn2  12404  mgm1  12617  sgrp1  12644  mhmima  12699  dfgrp2  12725  basgen2  12840  bastop1  12842  iscn  12956  cnpval  12957  iscnp  12958  iscnp3  12962  cnprcl2k  12965  lmbr  12972  lmbr2  12973  lmbrf  12974  cnptoprest  12998  cnptoprest2  12999  cnmpt21  13050  ispsmet  13082  ismet  13103  isxmet  13104  metss  13253  qtopbasss  13280  cncfval  13318  elcncf2  13320  mulc1cncf  13335  cncfmet  13338  dedekindeulemloc  13356  dedekindeulemeu  13359  dedekindeu  13360  suplociccreex  13361  dedekindicclemloc  13365  dedekindicclemeu  13368  dedekindicclemicc  13369  ivthinclemlopn  13373  ivthinclemlr  13374  ivthinclemuopn  13375  ivthinclemur  13376  ivthinclemloc  13378  limccl  13387  ellimc3apf  13388  limcdifap  13390  limcmpted  13391  2irrexpqap  13655  2sqlem6  13715  2sqlem10  13720  bj-charfunbi  13811  bj-omtrans  13956  strcoll2  13983  strcollnfALT  13986  sscoll2  13988  pw1nct  14001  0nninf  14002  nnsf  14003  peano4nninf  14004  nninfalllem1  14006  nninfself  14011  nninfsellemeq  14012  nninfsellemeqinf  14014  isomninnlem  14027  trilpolemlt1  14038  iswomninnlem  14046  iswomni0  14048  ismkvnnlem  14049  dceqnconst  14056  dcapnconst  14057