Theorem ralbidv 2494

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  ralbii  2500  2ralbidv  2518  rexralbidv  2520  r19.32vdc  2643  raleqbi1dv  2702  raleqbidv  2706  cbvral2vw  2737  cbvral2v  2739  rspceaimv  2873  rspc2  2876  rspc3v  2881  reu6i  2952  reu7  2956  sbcralt  3063  sbcralg  3065  raaanlem  3552  2ralunsn  3825  elintg  3879  elintrabg  3884  eliin  3918  brralrspcev  4088  bnd2  4203  poeq1  4331  soeq1  4347  frforeq1  4375  frforeq3  4379  frirrg  4382  frind  4384  weeq1  4388  reusv3  4492  ontr2exmid  4558  reg2exmidlema  4567  posng  4732  ralxpf  4809  cnvpom  5209  funcnvuni  5324  fnmptfvd  5663  dff4im  5705  dff13f  5814  eusvobj2  5905  ovanraleqv  5943  ofreq  6136  caofdig  6161  uchoice  6192  smoeq  6345  recseq  6361  tfr0dm  6377  tfrlemiex  6386  tfr1onlemex  6402  tfr1onlemaccex  6403  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllemex  6415  tfrcllemaccex  6416  tfrcllemres  6417  elixp2  6758  pw2f1odclem  6892  xpf1o  6902  nneneq  6915  ac6sfi  6956  fimax2gtrilemstep  6958  fimax2gtri  6959  opabfi  6994  supeq1  7047  supeq3  7051  supmoti  7054  eqsupti  7057  supubti  7060  suplubti  7061  supisoex  7070  cnvinfex  7079  eqinfti  7081  infvalti  7083  updjud  7143  ctssdclemr  7173  nninff  7183  nninfninc  7184  infnninf  7185  infnninfOLD  7186  nnnninf  7187  nnnninfeq  7189  nnnninfeq2  7190  enomnilem  7199  finomni  7201  exmidomni  7203  fodjuomnilemres  7209  ismkvnex  7216  fodjumkvlemres  7220  enmkvlem  7222  enwomnilem  7230  nninfdcinf  7232  nninfwlporlem  7234  nninfwlpoimlemg  7236  nninfwlpoimlemdc  7238  exmidontriimlem3  7285  exmidontriim  7287  tapeq1  7314  netap  7316  exmidapne  7322  cc2lem  7328  cc3  7330  elinp  7536  prloc  7553  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgpr  7744  caucvgprpr  7774  suplocexprlemloc  7783  suplocexpr  7787  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  caucvgsr  7864  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  axcaucvglemcau  7960  axcaucvglemres  7961  axpre-suploclemres  7963  axpre-suploc  7964  lbreu  8966  sup3exmid  8978  nnsub  9023  indstr  9661  supinfneg  9663  infsupneg  9664  ublbneg  9681  lbzbi  9684  iccsupr  10035  frecuzrdgsuc  10488  frecuzrdgg  10490  frecuzrdgsuctlem  10497  seq3f1olemstep  10588  seq3f1olemp  10589  seqfeq4g  10605  nn0ltexp2  10783  bccl  10841  cau4  11263  caubnd2  11264  maxleast  11360  rexanre  11367  rexico  11368  fimaxre2  11373  minmax  11376  xrminmax  11411  clim  11427  clim2  11429  clim2c  11430  clim0c  11432  climabs0  11453  cn1lem  11460  sumeq1  11501  prodeq1f  11698  zsupcllemstep  12085  infssuzex  12089  suprzubdc  12092  nninfdcex  12093  zsupssdc  12094  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlemex  12141  bezoutlemeu  12147  dfgcd3  12150  bezout  12151  dfgcd2  12154  nnwodc  12176  uzwodc  12177  nnwofdc  12178  sqrt2irr  12303  reumodprminv  12394  pc2dvds  12471  pcz  12473  prmpwdvds  12496  ennnfoneleminc  12571  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemnn0  12582  ennnfonelemr  12583  ennnfonelemim  12584  exmidunben  12586  ctinfomlemom  12587  ctinfom  12588  ctinf  12590  ctiunctlemudc  12597  ctiunct  12600  ssomct  12605  infpn2  12616  imasaddfnlemg  12900  mgm1  12956  sgrp1  12997  mhmima  13066  dfgrp2  13102  isgrpinv  13129  grpidinv  13134  dfgrp3mlem  13173  issubg4m  13266  isnsg2  13276  elnmz  13281  ghmrn  13330  ghmnsgima  13341  srgideu  13471  ring1  13558  lringuplu  13695  subrgugrp  13739  isrrg  13762  islssm  13856  islssmg  13857  rnglidlmcl  13979  basgen2  14260  bastop1  14262  iscn  14376  cnpval  14377  iscnp  14378  iscnp3  14382  cnprcl2k  14385  lmbr  14392  lmbr2  14393  lmbrf  14394  cnptoprest  14418  cnptoprest2  14419  cnmpt21  14470  ispsmet  14502  ismet  14523  isxmet  14524  metss  14673  qtopbasss  14700  cncfval  14751  elcncf2  14753  mulc1cncf  14768  cncfmet  14771  dedekindeulemloc  14798  dedekindeulemeu  14801  dedekindeu  14802  suplociccreex  14803  dedekindicclemloc  14807  dedekindicclemeu  14810  dedekindicclemicc  14811  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemloc  14820  ivthreinc  14824  dich0  14831  limccl  14838  ellimc3apf  14839  limcdifap  14841  limcmpted  14842  2irrexpqap  15151  2sqlem6  15277  2sqlem10  15282  bj-charfunbi  15373  bj-omtrans  15518  strcoll2  15545  strcollnfALT  15548  sscoll2  15550  pw1nct  15563  0nninf  15564  nnsf  15565  peano4nninf  15566  nninfalllem1  15568  nninfself  15573  nninfsellemeq  15574  nninfsellemeqinf  15576  isomninnlem  15590  trilpolemlt1  15601  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612  cndcap  15619  dceqnconst  15620  dcapnconst  15621  ltlenmkv  15630