Theorem ralbidv 2477

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  ralbii  2483  2ralbidv  2501  rexralbidv  2503  r19.32vdc  2626  raleqbi1dv  2680  raleqbidv  2684  cbvral2vw  2714  cbvral2v  2716  rspceaimv  2849  rspc2  2852  rspc3v  2857  reu6i  2928  reu7  2932  sbcralt  3039  sbcralg  3041  raaanlem  3528  2ralunsn  3798  elintg  3852  elintrabg  3857  eliin  3891  brralrspcev  4061  bnd2  4173  poeq1  4299  soeq1  4315  frforeq1  4343  frforeq3  4347  frirrg  4350  frind  4352  weeq1  4356  reusv3  4460  ontr2exmid  4524  reg2exmidlema  4533  posng  4698  ralxpf  4773  cnvpom  5171  funcnvuni  5285  fnmptfvd  5620  dff4im  5662  dff13f  5770  eusvobj2  5860  ovanraleqv  5898  ofreq  6085  smoeq  6290  recseq  6306  tfr0dm  6322  tfrlemiex  6331  tfr1onlemex  6347  tfr1onlemaccex  6348  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllemex  6360  tfrcllemaccex  6361  tfrcllemres  6362  elixp2  6701  xpf1o  6843  nneneq  6856  ac6sfi  6897  fimax2gtrilemstep  6899  fimax2gtri  6900  supeq1  6984  supeq3  6988  supmoti  6991  eqsupti  6994  supubti  6997  suplubti  6998  supisoex  7007  cnvinfex  7016  eqinfti  7018  infvalti  7020  updjud  7080  ctssdclemr  7110  nninff  7120  infnninf  7121  infnninfOLD  7122  nnnninf  7123  nnnninfeq  7125  nnnninfeq2  7126  enomnilem  7135  finomni  7137  exmidomni  7139  fodjuomnilemres  7145  ismkvnex  7152  fodjumkvlemres  7156  enmkvlem  7158  enwomnilem  7166  nninfdcinf  7168  nninfwlporlem  7170  nninfwlpoimlemg  7172  nninfwlpoimlemdc  7174  exmidontriimlem3  7221  exmidontriim  7223  tapeq1  7250  netap  7252  exmidapne  7258  cc2lem  7264  cc3  7266  elinp  7472  prloc  7489  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  caucvgpr  7680  caucvgprpr  7710  suplocexprlemloc  7719  suplocexpr  7723  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  caucvgsr  7800  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  axcaucvglemcau  7896  axcaucvglemres  7897  axpre-suploclemres  7899  axpre-suploc  7900  lbreu  8901  sup3exmid  8913  nnsub  8957  indstr  9592  supinfneg  9594  infsupneg  9595  ublbneg  9612  lbzbi  9615  iccsupr  9965  frecuzrdgsuc  10413  frecuzrdgg  10415  frecuzrdgsuctlem  10422  seq3f1olemstep  10500  seq3f1olemp  10501  nn0ltexp2  10688  bccl  10746  cau4  11124  caubnd2  11125  maxleast  11221  rexanre  11228  rexico  11229  fimaxre2  11234  minmax  11237  xrminmax  11272  clim  11288  clim2  11290  clim2c  11291  clim0c  11293  climabs0  11314  cn1lem  11321  sumeq1  11362  prodeq1f  11559  zsupcllemstep  11945  infssuzex  11949  suprzubdc  11952  nninfdcex  11953  zsupssdc  11954  bezoutlemstep  11997  bezoutlemmain  11998  bezoutlemex  12001  bezoutlemeu  12007  dfgcd3  12010  bezout  12011  dfgcd2  12014  nnwodc  12036  uzwodc  12037  nnwofdc  12038  sqrt2irr  12161  reumodprminv  12252  pc2dvds  12328  pcz  12330  prmpwdvds  12352  ennnfoneleminc  12411  ennnfonelemex  12414  ennnfonelemhom  12415  ennnfonelemnn0  12422  ennnfonelemr  12423  ennnfonelemim  12424  exmidunben  12426  ctinfomlemom  12427  ctinfom  12428  ctinf  12430  ctiunctlemudc  12437  ctiunct  12440  ssomct  12445  infpn2  12456  imasaddfnlemg  12734  mgm1  12788  sgrp1  12815  mhmima  12874  dfgrp2  12901  isgrpinv  12925  grpidinv  12928  dfgrp3mlem  12967  issubg4m  13051  isnsg2  13061  elnmz  13066  srgideu  13153  ring1  13234  lringuplu  13335  subrgugrp  13359  basgen2  13551  bastop1  13553  iscn  13667  cnpval  13668  iscnp  13669  iscnp3  13673  cnprcl2k  13676  lmbr  13683  lmbr2  13684  lmbrf  13685  cnptoprest  13709  cnptoprest2  13710  cnmpt21  13761  ispsmet  13793  ismet  13814  isxmet  13815  metss  13964  qtopbasss  13991  cncfval  14029  elcncf2  14031  mulc1cncf  14046  cncfmet  14049  dedekindeulemloc  14067  dedekindeulemeu  14070  dedekindeu  14071  suplociccreex  14072  dedekindicclemloc  14076  dedekindicclemeu  14079  dedekindicclemicc  14080  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemloc  14089  limccl  14098  ellimc3apf  14099  limcdifap  14101  limcmpted  14102  2irrexpqap  14366  2sqlem6  14437  2sqlem10  14442  bj-charfunbi  14533  bj-omtrans  14678  strcoll2  14705  strcollnfALT  14708  sscoll2  14710  pw1nct  14722  0nninf  14723  nnsf  14724  peano4nninf  14725  nninfalllem1  14727  nninfself  14732  nninfsellemeq  14733  nninfsellemeqinf  14735  isomninnlem  14748  trilpolemlt1  14759  iswomninnlem  14767  iswomni0  14769  ismkvnnlem  14770  dceqnconst  14777  dcapnconst  14778  ltlenmkv  14787