Theorem ralbidv 2725

Description: Formula-building rule for restricted universal quantifier (deduction rule). (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 1672	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	ralbid 2723	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wral 2705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710

This theorem is referenced by:  ralbii  2729  2ralbidv  2747  rexralbidv  2749  raleqbi1dv  2915  raleqbidv  2921  cbvral2v  2945  rspc2  3067  rspc3v  3071  reu6i  3139  reu7  3143  sbcralt  3255  raaan  3775  raaanv  3776  r19.12sn  3929  2ralunsn  4068  elintg  4124  elintrabg  4129  eliin  4164  disjprg  4276  disjxun  4278  reusv2lem2  4482  reusv3  4488  reusv6OLD  4491  poeq1  4631  somo  4662  frirr  4684  fr2nr  4685  frminex  4687  wereu2  4704  posn  4894  frsn  4896  ralxpf  4973  cnvpo  5363  fnmptfvd  5794  iinpreima  5821  dff4  5845  dff13f  5960  eusvobj2  6072  ofreq  6312  sorpssuni  6358  sorpssint  6359  fr3nr  6380  onssmin  6397  funcnvuni  6519  f1oweALT  6550  frxp  6671  smoeq  6797  recseq  6819  tfrlem12  6834  tz7.48lem  6882  elixp2  7255  undifixp  7287  xpf1o  7461  nneneq  7482  ac6sfi  7544  frfi  7545  fipreima  7605  indexfi  7607  marypha1lem  7671  marypha1  7672  supeq1  7683  supeq3  7687  supmo  7690  eqsup  7694  supub  7697  suplub  7698  supmaxlem  7702  supisoex  7709  oieq1  7714  ordtypecbv  7719  ordtypelem3  7722  ordtypelem6  7725  ordtypelem7  7726  ordtypelem9  7728  wemaplem1  7748  wemaplem2  7749  zfregcl  7797  oemapval  7879  oemapvali  7880  cantnf  7889  cantnfOLD  7911  wemapwe  7916  wemapweOLD  7917  rankval3b  8021  unbndrank  8037  rankunb  8045  rankuni2b  8048  tcrank  8079  scottex  8080  scottexs  8082  scott0s  8083  bnd2  8088  dfac8clem  8190  ac5num  8194  acni  8203  acni2  8204  alephval3  8268  dfac4  8280  dfac5lem5  8285  dfac5  8286  dfac2a  8287  dfac2  8288  dfacacn  8298  kmlem2  8308  kmlem13  8319  cflem  8403  cflecard  8410  cfeq0  8413  cfsuc  8414  cfflb  8416  cofsmo  8426  cfsmolem  8427  cfcoflem  8429  coftr  8430  alephsing  8433  fin23lem11  8474  isfin3ds  8486  fin23lem17  8495  fin23lem39  8507  isf33lem  8523  isf34lem6  8537  fin1a2lem13  8569  hsmexlem4  8586  hsmex  8589  axcc2lem  8593  axcc3  8595  dcomex  8604  axdc2lem  8605  axdc3lem2  8608  axdc3lem3  8609  axdc3  8611  axdc4lem  8612  axcclem  8614  zorn2lem2  8654  zorn2lem7  8659  zorn2g  8660  zornn0g  8662  ttukeylem7  8672  axdclem2  8677  brdom3  8683  brdom7disj  8686  brdom6disj  8687  alephval2  8724  inar1  8930  axgroth6  8983  pinq  9084  nqereu  9086  prlem934  9190  supexpr  9211  supsrlem  9266  axpre-sup  9324  dedekind  9521  dedekindle  9522  fimaxre2  10266  lbreu  10268  sup2  10274  infm3  10277  supmul1  10283  supmullem2  10285  supmul  10286  infmrcl  10297  nnsub  10348  uzwo  10905  uzwoOLD  10906  nnwof  10909  uzinfmi  10922  ublbneg  10927  lbzbi  10931  zsupss  10932  uzsupss  10935  uzwo3  10936  zmax  10938  rpnnen1lem1  10967  rpnnen1lem2  10968  rpnnen1lem3  10969  rpnnen1lem4  10970  rpnnen1lem5  10971  xrsupsslem  11257  xrinfmsslem  11258  xrsupss  11259  xrinfmss  11260  iccsupr  11370  supicc  11420  supiccub  11421  supicclub  11422  flval2  11646  flval3  11647  fsequb  11781  axdc4uzlem  11788  faclbnd4lem4  12056  bccl  12082  hashgt12el  12157  hashge2el2dif  12168  hashbc  12190  wrdind  12355  wrd2ind  12356  sqrlem3  12718  rexanre  12818  rexico  12825  cau4  12828  caubnd2  12829  caubnd  12830  clim  12956  rlim  12957  rlim2  12958  rlim2lt  12959  rlim3  12960  clim2  12966  clim2c  12967  clim0c  12969  rlim0  12970  rlim0lt  12971  ello12r  12979  ello1d  12985  lo1bdd2  12986  lo1bddrp  12987  elo12r  12990  rlimconst  13006  rlimresb  13027  rlimcld2  13040  climabs0  13047  rlimcn2  13052  reccn2  13058  cn1lem  13059  rlimo1  13078  o1rlimmul  13080  lo1add  13088  lo1mul  13089  isercoll  13129  caucvgrlem  13134  incexclem  13282  climcnds  13297  divrcnv  13298  ruclem12  13506  sqr2irr  13514  gcdcllem1  13678  gcdcllem2  13679  maxprmfct  13782  reumodprminv  13855  pc2dvds  13928  pcz  13930  prmpwdvds  13948  infpn2  13957  prmreclem1  13960  prmreclem2  13961  prmreclem3  13962  prmreclem5  13964  prmreclem6  13965  vdwlem6  14030  vdwlem8  14032  vdwlem13  14037  vdwnnlem1  14039  vdwnn  14042  ramz  14069  ramcl  14073  cshwrepswhash1  14112  prdsleval  14398  imasval  14432  imasaddfnlem  14449  imasvscafn  14458  mrisval  14551  isacs  14572  isacs2  14574  isacs1i  14578  mreacs  14579  acsfn  14580  acsfn2  14584  iscatd  14594  catidex  14595  catideu  14596  cidval  14598  catidd  14601  comfeq  14628  catpropd  14631  ismon  14655  isfunc  14757  isnat  14840  isprs  15083  drsdirfi  15091  ispos  15100  lubfval  15131  lubeldm  15134  lubval  15137  lubprop  15139  lublecllem  15141  glbfval  15144  glbeldm  15147  glbval  15150  glbprop  15152  joinval2lem  15161  joinlem  15164  meetval2lem  15175  meetlem  15178  isglbd  15270  lubl  15273  lubun  15276  clatleglb  15279  poslubmo  15299  posglbmo  15300  poslubd  15301  ipodrsima  15318  isdlat  15346  mgmidmo  15401  ismgmid  15418  ismgmid2  15421  ismndd  15427  mhmima  15473  mrcmndind  15476  gsumvallem1  15482  gsumvallem2  15483  gsumvalx  15484  gsumress  15487  gsumval2  15493  gsumwspan  15504  isgrpinv  15568  issubg4  15680  0subg  15686  cycsubgcl  15687  isnsg2  15691  nsgacs  15697  elnmz  15700  ghmrn  15740  ghmnsgima  15750  isga  15789  orbsta  15811  cntzfval  15818  elcntz  15820  resscntz  15829  oppgsubg  15858  symgextfo  15907  gsmsymgreqlem2  15916  gsmsymgreq  15917  pmtrdifel  15966  pmtrdifwrdellem3  15969  pmtrdifwrdel  15971  pmtrdifwrdel2  15972  psgnunilem2  15981  psgnunilem3  15982  odeq  16033  gexid  16060  gexlem2  16061  gexdvds  16063  isslw  16087  pgpssslw  16093  sylow2alem1  16096  sylow2alem2  16097  efgval  16194  efgrelexlemb  16227  efgcpbllemb  16232  gexex  16315  dmdprd  16454  dprd2da  16515  pgpfac1lem5  16554  isabv  16828  islss  16938  lssacs  16970  reslmhm  17055  islbs  17079  pj1lmhm  17103  lbsacsbs  17159  isrrg  17281  opsrval  17488  zringlpir  17748  zlpir  17753  psgndiflemA  17873  ocvfval  17933  elocv  17935  iunocv  17948  frlmlbs  18067  islindf  18083  islinds2  18084  islindf2  18085  lindfrn  18092  lsslindf  18101  islindf4  18109  mdetunilem1  18260  mdetunilem9  18268  basgen2  18436  bastop1  18440  isclo  18533  ordtbaslem  18634  iscn  18681  cnpval  18682  iscnp  18683  iscnp3  18690  lmbr  18704  lmbr2  18705  lmbrf  18706  cnprest  18735  cnprest2  18736  t0sep  18770  isreg  18778  t1sep2  18815  tgcmp  18846  1stcclb  18890  1stcfb  18891  2ndc1stc  18897  1stcrest  18899  2ndcdisj  18902  islly  18914  isnlly  18915  lly1stc  18942  elkgen  18951  kgencn  18971  elpt  18987  elptr  18988  ptcnplem  19036  tx1stc  19065  cnmpt21  19086  kqt0lem  19151  isr0  19152  regr1lem2  19155  r0sep  19163  nrmr0reg  19164  flffbas  19410  cnflf  19417  cnflf2  19418  lmflf  19420  txflf  19421  fclsopni  19430  fclsnei  19434  fclsrest  19439  fcfnei  19450  cnfcf  19457  alexsubb  19460  alexsubALTlem3  19463  divstgplem  19533  tsmsfbas  19540  tsmsgsum  19551  tsmsgsumOLD  19554  tsmsresOLD  19559  tsmsres  19560  tsmsf1o  19561  tsmsxplem1  19569  tsmsxp  19571  ustval  19619  isust  19620  ustincl  19624  ustdiag  19625  ustinvel  19626  ustexhalf  19627  ust0  19636  utopval  19649  ucnval  19694  isucn  19695  isucn2  19696  ucnima  19698  iscfilu  19705  ispsmet  19722  ismet  19740  isxmet  19741  imasdsf1olem  19790  imasf1oxmet  19792  imasf1omet  19793  metss  19925  met1stc  19938  prdsxmslem2  19946  metcnpi3  19963  txmetcnp  19964  metucnOLD  20005  metucn  20006  nlmvscn  20110  nrginvrcnlem  20113  nmoval  20136  nmolb  20138  nghmcn  20166  qtopbaslem  20179  icccmplem2  20242  icccmplem3  20243  reconnlem2  20246  metdscn  20274  cncfval  20306  elcncf2  20308  elcncf1di  20313  mulc1cncf  20323  cncfmet  20326  cnllycmp  20370  evth  20373  lebnumlem3  20377  lebnum  20378  xlebnum  20379  ishtpy  20386  isphtpy  20395  pi1xfr  20469  pi1coghm  20475  ipcn  20600  lmmbr2  20612  lmmbr3  20613  lmmbrf  20615  cfilfval  20617  iscfil  20618  fmcfil  20625  caufval  20628  iscau  20629  iscau2  20630  iscau3  20631  iscau4  20632  iscauf  20633  caucfil  20636  cfilresi  20648  causs  20651  lmclim  20655  cncmet  20675  cmetcusp1OLD  20705  cmetcusp1  20706  minveclem4c  20754  minveclem2  20755  minveclem3b  20757  minveclem4  20761  minveclem6  20763  minveclem7  20764  ivthlem2  20778  ivthlem3  20779  cniccbdd  20787  ovolunlem1  20822  ovoliunlem1  20827  ovoliun2  20831  ovolicc2lem3  20844  ismbl  20851  ioombl1lem4  20884  uniioombllem2  20905  uniioombllem6  20910  dyadmax  20920  dyadmbllem  20921  dyadmbl  20922  opnmbllem  20923  volcn  20928  ismbf1  20946  ismbf  20950  mbfeqalem  20962  mbfinf  20985  mbflimsup  20986  itg1climres  21034  mbfi1fseqlem6  21040  mbfi1flimlem  21042  itg2seq  21062  itg2monolem1  21070  itg2i1fseq  21075  itg2i1fseq2  21076  itg2cnlem1  21081  itg2cnlem2  21082  isibl  21085  dveflem  21293  ply1divex  21493  fta1g  21524  plyeq0lem  21563  dgrco  21627  plydivex  21648  fta1  21659  vieta1  21663  aannenlem1  21679  aannenlem2  21680  aalioulem2  21684  aalioulem3  21685  ulmval  21730  ulm2  21735  ulmi  21736  ulmres  21738  ulmshftlem  21739  ulmcaulem  21744  ulmcau  21745  ulmss  21747  ulmbdd  21748  ulmdvlem1  21750  ulmdvlem3  21752  mtestbdd  21755  iblulm  21757  abelthlem8  21789  pilem2  21802  pilem3  21803  divlogrlim  21965  cxpcn3  22071  dmarea  22236  rlimcnp  22244  cxplim  22250  cxploglim  22256  scvxcvx  22264  emcllem6  22279  ftalem1  22295  ftalem2  22296  ftalem3  22297  isppw2  22338  perfectlem2  22454  2sqlem6  22593  2sqlem10  22598  dchrisumlema  22622  dchrisumlem2  22624  dchrisumlem3  22625  dchrisum0  22654  pntpbnd  22722  pntibndlem3  22726  pntibnd  22727  pntleme  22742  pntlem3  22743  pntlemp  22744  pnt3  22746  axtg5seg  22811  brbtwn2  22974  colinearalg  22979  axsegconlem1  22986  axsegcon  22996  ax5seglem4  23001  ax5seglem5  23002  axlowdim  23030  axeuclidlem  23031  axcontlem1  23033  axcontlem2  23034  axcontlem4  23036  axcontlem5  23037  axcontlem8  23040  axcontlem12  23044  cusgra3v  23195  wlks  23248  wlkntrllem3  23283  constr3trllem2  23360  1conngra  23384  iseupa  23409  isgrpo  23506  isgrpo2  23507  isgrpoi  23508  grpoideu  23519  grpoidinv2  23528  isgrp2d  23545  isgrpda  23607  exidu1  23636  cmpidelt  23639  cnid  23661  mulid  23666  ghgrp  23678  isrngod  23689  rngoideu  23694  cnrngo  23713  vci  23749  isvclem  23778  isnvlem  23811  nvi  23815  nmcvcn  23913  lnoval  23975  islno  23976  isblo3i  24024  blo3i  24025  blocnilem  24027  blocni  24028  ajfval  24032  ubthlem1  24094  ubthlem2  24095  ubthlem3  24096  ubth  24097  minvecolem2  24099  minvecolem3  24100  minvecolem4c  24103  minvecolem4  24104  minvecolem5  24105  minvecolem6  24106  minvecolem7  24107  htthlem  24142  h2hcau  24204  h2hlm  24205  hilid  24386  hcau  24409  hlimi  24413  hlim2  24417  ocel  24507  adjsym  25060  ellnop  25085  ellnfn  25110  hhcno  25131  hhcnf  25132  0cnop  25206  0cnfn  25207  idcnop  25208  lnopeq  25236  elunop2  25240  lnophm  25246  lnconi  25260  lnopcnbd  25263  lnfncnbd  25284  imaelshi  25285  riesz3i  25289  riesz4i  25290  riesz4  25291  riesz1  25292  cnlnadjlem2  25295  cnlnadjlem5  25298  cnlnadjlem8  25301  cnlnadji  25303  nmopadjlei  25315  cnvbraval  25337  leopg  25349  leoppos  25353  mdbr  25521  dmdbr  25526  cdj3i  25668  rmoeq  25695  disjunsn  25760  funcnv5mpt  25812  fgreu  25814  resspos  25943  isomnd  25988  inftmrel  26021  isinftm  26022  archiabl  26039  rngurd  26109  isarchiofld  26138  rge0scvg  26233  qqhcn  26274  esumpcvgval  26381  sigaval  26407  issgon  26420  isrnmeas  26468  ismbfm  26521  isanmbfm  26525  mbfmcst  26528  sitgval  26566  oddpwdc  26585  eulerpartlemd  26597  ballotleme  26727  signsw0g  26805  signswmnd  26806  lgamgulmlem2  26864  lgamgulmlem3  26865  lgamgulmlem5  26867  lgambdd  26871  lgamcvglem  26874  derangenlem  26907  subfacp1lem3  26918  subfacp1lem5  26920  subfacp1lem6  26921  subfacp1  26922  erdszelem8  26934  kur14  26952  cnpcon  26967  rescon  26983  cvmscbv  26995  iscvm  26996  cvmsi  27002  cvmsval  27003  cvmlift3lem2  27057  snmlval  27068  ghomgrpilem1  27151  dfpo2  27412  dfon2lem9  27451  dfrdg2  27456  dfrdg3  27457  poseq  27561  soseq  27562  wrecseq123  27565  wfrlem1  27571  wfrlem15  27585  frrlem1  27615  sltval  27635  nocvxminlem  27678  nobndlem2  27681  nobndlem8  27687  nobndup  27688  nobnddown  27689  fin2so  28260  supaddc  28261  supadd  28262  heicant  28270  mblfinlem1  28272  mblfinlem2  28273  mblfinlem3  28274  ismblfin  28276  voliunnfl  28279  volsupnfl  28280  mbfresfi  28282  itg2addnc  28290  ftc1anc  28319  nn0prpwlem  28361  isfne  28384  isfne4  28385  isfne2  28387  isfne3  28388  isref  28395  islocfin  28412  neibastop3  28427  topmeet  28429  topjoin  28430  filnetlem4  28446  f1opr  28462  upixp  28467  indexdom  28472  filbcmb  28478  sdclem2  28482  fdc  28485  lmclim2  28498  caures  28500  istotbnd  28512  istotbnd3  28514  sstotbnd  28518  isbnd  28523  heibor  28564  bfp  28567  rrncmslem  28575  exidres  28587  exidresid  28588  idlval  28657  isidl  28658  0idl  28669  unichnidl  28675  pridl  28681  ismaxidl  28684  smprngopr  28696  igenval2  28710  prnc  28711  ispridlc  28714  scottexf  28825  scott0f  28826  isnacs  28885  isnacs2  28887  nacsfix  28893  mzpclval  28906  elmzpcl  28907  rencldnfilem  29004  infmrgelbi  29064  pellfundre  29067  pellfundlb  29070  wepwsolem  29239  fnwe2lem2  29249  aomclem8  29259  dfac11  29260  gicabl  29299  islnr3  29316  hbtlem2  29325  hbtlem5  29329  evth2f  29582  ubelsupr  29587  evthf  29594  fnchoice  29596  stoweidlem5  29646  stoweidlem9  29650  stoweidlem15  29656  stoweidlem16  29657  stoweidlem27  29668  stoweidlem28  29669  stoweidlem31  29672  stoweidlem34  29675  stoweidlem37  29678  stoweidlem46  29687  stoweidlem48  29689  stoweidlem51  29692  stoweidlem52  29693  stoweidlem59  29700  wallispilem3  29708  stirlinglem13  29727  cbvral2  29842  raaan2  29845  2reu4a  29859  dfdfat2  29883  wlkelwrd  30126  wlkcompim  30133  wwlk  30161  clwwlk  30275  rusgra0edg  30419  frgrawopreg1  30489  frgrawopreg2  30490  frgrareg  30556  frgraregord013  30557  mat0dimcrng  30646  linindslinci  30691  lindslinindsimp1  30700  lindslinindsimp2lem5  30705  lindslinindsimp2  30706  linds0  30708  lindsrng01  30711  snlindsntor  30714  mnd1  30730  grp1  30731  abl1  30732  rng1  30734  lmod1  30743  ldepsnlinc  30759  bnj1185  31489  bnj1385  31528  bnj66  31555  bnj106  31563  bnj155  31574  bnj852  31616  bnj893  31623  bnj1228  31704  bnj1234  31706  bnj1463  31748  riotasvd  32180  islfl  32278  eqlkr  32317  eqlkr3  32319  glbconN  32594  hlsuprexch  32598  ispsubsp  32962  ldilset  33326  isldil  33327  dilsetN  33370  isdilN  33371  trlset  33378  trlval  33379  cdleme27b  33585  cdleme29b  33592  cdleme31so  33596  cdleme31sn1  33598  cdleme31sn1c  33605  cdleme31fv  33607  cdleme40v  33686  istendo  33977  cdlemkid3N  34150  cdlemkid4  34151  cdlemkid5  34152  dihfval  34449  dihval  34450  islpolN  34701  hdmapffval  35047  hdmapfval  35048  hdmapval  35049  hdmapval2lem  35052  hgmapffval  35106  hgmapfval  35107  hgmapval  35108  hgmapvs  35112  taupilemrplb  35187