Theorem ralbidv 2464

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

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

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 1434  ax-gen 1436  ax-4 1497  ax-17 1513

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-ral 2447

This theorem is referenced by:  ralbii  2470  2ralbidv  2488  rexralbidv  2490  r19.32vdc  2613  raleqbi1dv  2667  raleqbidv  2671  cbvral2v  2700  rspceaimv  2833  rspc2  2836  rspc3v  2841  reu6i  2912  reu7  2916  sbcralt  3022  sbcralg  3024  raaanlem  3509  2ralunsn  3772  elintg  3826  elintrabg  3831  eliin  3865  brralrspcev  4034  bnd2  4146  poeq1  4271  soeq1  4287  frforeq1  4315  frforeq3  4319  frirrg  4322  frind  4324  weeq1  4328  reusv3  4432  ontr2exmid  4496  reg2exmidlema  4505  posng  4670  ralxpf  4744  cnvpom  5140  funcnvuni  5251  dff4im  5625  dff13f  5732  eusvobj2  5822  ovanraleqv  5860  ofreq  6047  smoeq  6249  recseq  6265  tfr0dm  6281  tfrlemiex  6290  tfr1onlemex  6306  tfr1onlemaccex  6307  tfrcllemsucaccv  6313  tfrcllembxssdm  6315  tfrcllemex  6319  tfrcllemaccex  6320  tfrcllemres  6321  elixp2  6659  xpf1o  6801  nneneq  6814  ac6sfi  6855  fimax2gtrilemstep  6857  fimax2gtri  6858  supeq1  6942  supeq3  6946  supmoti  6949  eqsupti  6952  supubti  6955  suplubti  6956  supisoex  6965  cnvinfex  6974  eqinfti  6976  infvalti  6978  updjud  7038  ctssdclemr  7068  nninff  7078  infnninf  7079  infnninfOLD  7080  nnnninf  7081  nnnninfeq  7083  nnnninfeq2  7084  enomnilem  7093  finomni  7095  exmidomni  7097  fodjuomnilemres  7103  ismkvnex  7110  fodjumkvlemres  7114  enmkvlem  7116  enwomnilem  7124  exmidontriimlem3  7170  exmidontriim  7172  cc2lem  7198  cc3  7200  elinp  7406  prloc  7423  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  caucvgpr  7614  caucvgprpr  7644  suplocexprlemloc  7653  suplocexpr  7657  caucvgsrlemgt1  7727  caucvgsrlemoffres  7732  caucvgsr  7734  suplocsrlemb  7738  suplocsrlempr  7739  suplocsrlem  7740  axcaucvglemcau  7830  axcaucvglemres  7831  axpre-suploclemres  7833  axpre-suploc  7834  lbreu  8831  sup3exmid  8843  nnsub  8887  indstr  9522  supinfneg  9524  infsupneg  9525  ublbneg  9542  lbzbi  9545  iccsupr  9893  frecuzrdgsuc  10339  frecuzrdgg  10341  frecuzrdgsuctlem  10348  seq3f1olemstep  10426  seq3f1olemp  10427  nn0ltexp2  10612  bccl  10669  cau4  11044  caubnd2  11045  maxleast  11141  rexanre  11148  rexico  11149  fimaxre2  11154  minmax  11157  xrminmax  11192  clim  11208  clim2  11210  clim2c  11211  clim0c  11213  climabs0  11234  cn1lem  11241  sumeq1  11282  prodeq1f  11479  zsupcllemstep  11863  infssuzex  11867  suprzubdc  11870  nninfdcex  11871  zsupssdc  11872  bezoutlemstep  11915  bezoutlemmain  11916  bezoutlemex  11919  bezoutlemeu  11925  dfgcd3  11928  bezout  11929  dfgcd2  11932  sqrt2irr  12071  reumodprminv  12162  pc2dvds  12238  pcz  12240  ennnfoneleminc  12281  ennnfonelemex  12284  ennnfonelemhom  12285  ennnfonelemnn0  12292  ennnfonelemr  12293  ennnfonelemim  12294  exmidunben  12296  ctinfomlemom  12297  ctinfom  12298  ctinf  12300  ctiunctlemudc  12307  ctiunct  12310  ssomct  12315  basgen2  12622  bastop1  12624  iscn  12738  cnpval  12739  iscnp  12740  iscnp3  12744  cnprcl2k  12747  lmbr  12754  lmbr2  12755  lmbrf  12756  cnptoprest  12780  cnptoprest2  12781  cnmpt21  12832  ispsmet  12864  ismet  12885  isxmet  12886  metss  13035  qtopbasss  13062  cncfval  13100  elcncf2  13102  mulc1cncf  13117  cncfmet  13120  dedekindeulemloc  13138  dedekindeulemeu  13141  dedekindeu  13142  suplociccreex  13143  dedekindicclemloc  13147  dedekindicclemeu  13150  dedekindicclemicc  13151  ivthinclemlopn  13155  ivthinclemlr  13156  ivthinclemuopn  13157  ivthinclemur  13158  ivthinclemloc  13160  limccl  13169  ellimc3apf  13170  limcdifap  13172  limcmpted  13173  2irrexpqap  13437  bj-charfunbi  13528  bj-omtrans  13673  strcoll2  13700  strcollnfALT  13703  sscoll2  13705  pw1nct  13717  0nninf  13718  nnsf  13719  peano4nninf  13720  nninfalllem1  13722  nninfself  13727  nninfsellemeq  13728  nninfsellemeqinf  13730  isomninnlem  13743  trilpolemlt1  13754  iswomninnlem  13762  iswomni0  13764  ismkvnnlem  13765  dceqnconst  13772  dcapnconst  13773