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  2681  raleqbidv  2685  cbvral2vw  2715  cbvral2v  2717  rspceaimv  2850  rspc2  2853  rspc3v  2858  reu6i  2929  reu7  2933  sbcralt  3040  sbcralg  3042  raaanlem  3529  2ralunsn  3799  elintg  3853  elintrabg  3858  eliin  3892  brralrspcev  4062  bnd2  4174  poeq1  4300  soeq1  4316  frforeq1  4344  frforeq3  4348  frirrg  4351  frind  4353  weeq1  4357  reusv3  4461  ontr2exmid  4525  reg2exmidlema  4534  posng  4699  ralxpf  4774  cnvpom  5172  funcnvuni  5286  fnmptfvd  5621  dff4im  5663  dff13f  5771  eusvobj2  5861  ovanraleqv  5899  ofreq  6086  smoeq  6291  recseq  6307  tfr0dm  6323  tfrlemiex  6332  tfr1onlemex  6348  tfr1onlemaccex  6349  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllemex  6361  tfrcllemaccex  6362  tfrcllemres  6363  elixp2  6702  xpf1o  6844  nneneq  6857  ac6sfi  6898  fimax2gtrilemstep  6900  fimax2gtri  6901  supeq1  6985  supeq3  6989  supmoti  6992  eqsupti  6995  supubti  6998  suplubti  6999  supisoex  7008  cnvinfex  7017  eqinfti  7019  infvalti  7021  updjud  7081  ctssdclemr  7111  nninff  7121  infnninf  7122  infnninfOLD  7123  nnnninf  7124  nnnninfeq  7126  nnnninfeq2  7127  enomnilem  7136  finomni  7138  exmidomni  7140  fodjuomnilemres  7146  ismkvnex  7153  fodjumkvlemres  7157  enmkvlem  7159  enwomnilem  7167  nninfdcinf  7169  nninfwlporlem  7171  nninfwlpoimlemg  7173  nninfwlpoimlemdc  7175  exmidontriimlem3  7222  exmidontriim  7224  tapeq1  7251  netap  7253  exmidapne  7259  cc2lem  7265  cc3  7267  elinp  7473  prloc  7490  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgpr  7681  caucvgprpr  7711  suplocexprlemloc  7720  suplocexpr  7724  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  caucvgsr  7801  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  axcaucvglemcau  7897  axcaucvglemres  7898  axpre-suploclemres  7900  axpre-suploc  7901  lbreu  8902  sup3exmid  8914  nnsub  8958  indstr  9593  supinfneg  9595  infsupneg  9596  ublbneg  9613  lbzbi  9616  iccsupr  9966  frecuzrdgsuc  10414  frecuzrdgg  10416  frecuzrdgsuctlem  10423  seq3f1olemstep  10501  seq3f1olemp  10502  nn0ltexp2  10689  bccl  10747  cau4  11125  caubnd2  11126  maxleast  11222  rexanre  11229  rexico  11230  fimaxre2  11235  minmax  11238  xrminmax  11273  clim  11289  clim2  11291  clim2c  11292  clim0c  11294  climabs0  11315  cn1lem  11322  sumeq1  11363  prodeq1f  11560  zsupcllemstep  11946  infssuzex  11950  suprzubdc  11953  nninfdcex  11954  zsupssdc  11955  bezoutlemstep  11998  bezoutlemmain  11999  bezoutlemex  12002  bezoutlemeu  12008  dfgcd3  12011  bezout  12012  dfgcd2  12015  nnwodc  12037  uzwodc  12038  nnwofdc  12039  sqrt2irr  12162  reumodprminv  12253  pc2dvds  12329  pcz  12331  prmpwdvds  12353  ennnfoneleminc  12412  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemnn0  12423  ennnfonelemr  12424  ennnfonelemim  12425  exmidunben  12427  ctinfomlemom  12428  ctinfom  12429  ctinf  12431  ctiunctlemudc  12438  ctiunct  12441  ssomct  12446  infpn2  12457  imasaddfnlemg  12735  mgm1  12789  sgrp1  12816  mhmima  12875  dfgrp2  12902  isgrpinv  12926  grpidinv  12929  dfgrp3mlem  12968  issubg4m  13053  isnsg2  13063  elnmz  13068  srgideu  13155  ring1  13236  lringuplu  13337  subrgugrp  13361  basgen2  13584  bastop1  13586  iscn  13700  cnpval  13701  iscnp  13702  iscnp3  13706  cnprcl2k  13709  lmbr  13716  lmbr2  13717  lmbrf  13718  cnptoprest  13742  cnptoprest2  13743  cnmpt21  13794  ispsmet  13826  ismet  13847  isxmet  13848  metss  13997  qtopbasss  14024  cncfval  14062  elcncf2  14064  mulc1cncf  14079  cncfmet  14082  dedekindeulemloc  14100  dedekindeulemeu  14103  dedekindeu  14104  suplociccreex  14105  dedekindicclemloc  14109  dedekindicclemeu  14112  dedekindicclemicc  14113  ivthinclemlopn  14117  ivthinclemlr  14118  ivthinclemuopn  14119  ivthinclemur  14120  ivthinclemloc  14122  limccl  14131  ellimc3apf  14132  limcdifap  14134  limcmpted  14135  2irrexpqap  14399  2sqlem6  14470  2sqlem10  14475  bj-charfunbi  14566  bj-omtrans  14711  strcoll2  14738  strcollnfALT  14741  sscoll2  14743  pw1nct  14755  0nninf  14756  nnsf  14757  peano4nninf  14758  nninfalllem1  14760  nninfself  14765  nninfsellemeq  14766  nninfsellemeqinf  14768  isomninnlem  14781  trilpolemlt1  14792  iswomninnlem  14800  iswomni0  14802  ismkvnnlem  14803  dceqnconst  14810  dcapnconst  14811  ltlenmkv  14820