Theorem ralbidv 2550

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralbii  2556  2ralbidv  2574  rexralbidv  2576  r19.32vdc  2700  raleqbi1dv  2761  raleqbidv  2765  cbvral2vw  2797  cbvral2v  2799  rspceaimv  2938  rspc2  2941  rspc3v  2946  reu6i  3017  reu7  3021  sbcralt  3128  sbcralg  3130  reu8nf  3133  raaanlem  3632  2ralunsn  3924  elintg  3978  elintrabg  3983  eliin  4017  brralrspcev  4189  bnd2  4310  poeq1  4444  soeq1  4460  frforeq1  4488  frforeq3  4492  frirrg  4495  frind  4497  weeq1  4501  reusv3  4606  ontr2exmid  4672  reg2exmidlema  4681  posng  4847  ralxpf  4926  cnvpom  5330  funcnvuni  5450  fnmptfvd  5813  dff4im  5854  dff13f  5976  eusvobj2  6071  ovanraleqv  6109  ofreq  6306  caofdig  6336  uchoice  6371  suppssrst  6501  suppssrgst  6502  suppofss1dcl  6504  suppofss2dcl  6505  smoeq  6561  recseq  6577  tfr0dm  6593  tfrlemiex  6602  tfr1onlemex  6618  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemex  6631  tfrcllemaccex  6632  tfrcllemres  6633  elixp2  6984  pw2f1odclem  7134  xpf1o  7144  nneneq  7158  ac6sfi  7202  fimax2gtrilemstep  7205  fimax2gtri  7206  elssdc  7209  opabfi  7247  2omap  7318  supeq1  7326  supeq3  7330  supmoti  7333  eqsupti  7336  supubti  7339  suplubti  7340  supisoex  7349  cnvinfex  7358  eqinfti  7360  infvalti  7362  updjud  7422  ctssdclemr  7452  nninff  7462  nninfninc  7463  infnninf  7464  infnninfOLD  7465  nnnninf  7466  nnnninfeq  7468  nnnninfeq2  7469  enomnilem  7478  finomni  7480  exmidomni  7482  fodjuomnilemres  7488  ismkvnex  7495  fodjumkvlemres  7499  enmkvlem  7501  enwomnilem  7509  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemg  7515  nninfwlpoimlemdc  7517  exmidontriimlem3  7579  exmidontriim  7581  papeq1  7609  papsym  7612  papcotr  7613  tapeq1  7618  netap  7620  exmidapne  7626  cc2lem  7632  cc3  7634  elinp  7841  prloc  7858  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgpr  8049  caucvgprpr  8079  suplocexprlemloc  8088  suplocexpr  8092  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  lbreu  9277  sup3exmid  9289  nnsub  9345  indstr  10002  supinfneg  10004  infsupneg  10005  ublbneg  10022  lbzbi  10025  iccsupr  10378  zsupcllemstep  10672  infssuzex  10676  suprzubdc  10681  nninfdcex  10682  zsupssdc  10683  frecuzrdgsuc  10864  frecuzrdgg  10866  frecuzrdgsuctlem  10873  seq3f1olemstep  10964  seq3f1olemp  10965  seqfeq4g  10981  nn0ltexp2  11161  bccl  11219  hashfibc  11297  wrdind  11508  wrd2ind  11509  cau4  11897  caubnd2  11898  maxleast  11994  rexanre  12001  rexico  12002  fimaxre2  12008  minmax  12011  xrminmax  12047  clim  12063  clim2  12065  clim2c  12066  clim0c  12068  climabs0  12089  cn1lem  12096  sumeq1  12137  prodeq1f  12335  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlemex  12794  bezoutlemeu  12800  dfgcd3  12803  bezout  12804  dfgcd2  12807  nnwodc  12829  uzwodc  12830  nnwofdc  12831  sqrt2irr  12957  reumodprminv  13052  pc2dvds  13129  pcz  13131  prmpwdvds  13154  ballotfileme  13285  ennnfoneleminc  13351  ennnfonelemex  13354  ennnfonelemhom  13355  ennnfonelemnn0  13362  ennnfonelemr  13363  ennnfonelemim  13364  exmidunben  13366  ctinfomlemom  13367  ctinfom  13368  ctinf  13370  ctiunctlemudc  13377  ctiunct  13380  ssomct  13385  infpn2  13396  imasaddfnlemg  13684  mgm1  13739  sgrp1  13775  mhmima  13847  dfgrp2  13881  isgrpinv  13908  grpidinv  13913  dfgrp3mlem  13952  issubg4m  14045  isnsg2  14055  elnmz  14060  ghmrn  14109  ghmnsgima  14120  srgideu  14325  ring1  14413  lringuplu  14552  subrgugrp  14597  isrrg  14620  islssm  14743  islssmg  14744  rnglidlmcl  14866  isassa  15051  mplsubgfilemm  15138  mplsubgfilemcl  15139  basgen2  15231  bastop1  15233  iscn  15347  cnpval  15348  iscnp  15349  iscnp3  15353  cnprcl2k  15356  lmbr  15363  lmbr2  15364  lmbrf  15365  cnptoprest  15389  cnptoprest2  15390  cnmpt21  15441  ispsmet  15473  ismet  15494  isxmet  15495  metss  15644  qtopbasss  15671  cncfval  15722  elcncf2  15724  mulc1cncf  15739  cncfmet  15742  dedekindeulemloc  15769  dedekindeulemeu  15772  dedekindeu  15773  suplociccreex  15774  dedekindicclemloc  15778  dedekindicclemeu  15781  dedekindicclemicc  15782  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemloc  15791  ivthreinc  15795  dich0  15802  limccl  15809  ellimc3apf  15810  limcdifap  15812  limcmpted  15813  2irrexpqap  16133  zprmlogbaplem2  16135  zprmlogbap  16137  perfectlem2  16198  prmefexple  16206  bposlem1  16209  2sqlem6  16337  2sqlem10  16342  wksfval  16661  wlkvtxedg  16702  clwwlkg  16732  depind  16848  bj-charfunbi  16935  bj-omtrans  17080  strcoll2  17107  strcollnfALT  17110  sscoll2  17112  pw1nct  17131  exmidcon  17135  0nninf  17145  nnsf  17146  peano4nninf  17147  nninfalllem1  17149  nninfself  17154  nninfsellemeq  17155  nninfsellemeqinf  17157  isomninnlem  17177  trilpolemlt1  17188  iswomninnlem  17197  iswomni0  17199  ismkvnnlem  17200  cndcap  17207  dceqnconst  17208  dcapnconst  17209  ltlenmkv  17218