Theorem ralbidv 2882

Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

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		ralbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 465	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	ralbidva 2879	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1804   A.wral 2793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691

This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2798

This theorem is referenced by:  2ralbidv  2887  ralbiiOLD  2957  rexralbidv  2962  raleqbi1dv  3048  raleqbidv  3054  cbvral2v  3078  rspc2  3204  rspc3v  3208  reu6i  3276  reu7  3280  sbcralt  3394  raaan  3922  raaanv  3923  2ralsng  4051  r19.12snOLD  4081  2ralunsn  4223  elintg  4279  elintrabg  4284  eliin  4321  disjprg  4433  disjxun  4435  reusv2lem2  4639  reusv3  4645  reusv6OLD  4648  poeq1  4793  somo  4824  frirr  4846  fr2nr  4847  frminex  4849  wereu2  4866  posn  5058  frsn  5060  ralxpf  5139  cnvpo  5535  fnmptfvd  5975  iinpreima  6002  dff4  6030  dff13f  6152  eusvobj2  6274  ofreq  6528  sorpssuni  6574  sorpssint  6575  fr3nr  6600  onssmin  6617  funcnvuni  6738  f1oweALT  6769  frxp  6895  smoeq  7023  recseq  7045  tfrlem12  7060  tz7.48lem  7108  elixp2  7475  undifixp  7507  xpf1o  7681  nneneq  7702  ac6sfi  7766  frfi  7767  fipreima  7828  indexfi  7830  marypha1lem  7895  marypha1  7896  supeq1  7907  supeq3  7911  supmo  7914  eqsup  7918  supub  7921  suplub  7922  supmaxlemOLD  7927  supisoex  7935  oieq1  7940  ordtypecbv  7945  ordtypelem3  7948  ordtypelem6  7951  ordtypelem7  7952  ordtypelem9  7954  wemaplem1  7974  wemaplem2  7975  zfregcl  8023  oemapval  8105  oemapvali  8106  cantnf  8115  cantnfOLD  8137  wemapwe  8142  wemapweOLD  8143  rankval3b  8247  unbndrank  8263  rankunb  8271  rankuni2b  8274  tcrank  8305  scottex  8306  scottexs  8308  scott0s  8309  bnd2  8314  dfac8clem  8416  ac5num  8420  acni  8429  acni2  8430  alephval3  8494  dfac4  8506  dfac5lem5  8511  dfac5  8512  dfac2a  8513  dfac2  8514  dfacacn  8524  kmlem2  8534  kmlem13  8545  cflem  8629  cflecard  8636  cfeq0  8639  cfsuc  8640  cfflb  8642  cofsmo  8652  cfsmolem  8653  cfcoflem  8655  coftr  8656  alephsing  8659  fin23lem11  8700  isfin3ds  8712  fin23lem17  8721  fin23lem39  8733  isf33lem  8749  isf34lem6  8763  fin1a2lem13  8795  hsmexlem4  8812  hsmex  8815  axcc2lem  8819  axcc3  8821  dcomex  8830  axdc2lem  8831  axdc3lem2  8834  axdc3lem3  8835  axdc3  8837  axdc4lem  8838  axcclem  8840  zorn2lem2  8880  zorn2lem7  8885  zorn2g  8886  zornn0g  8888  ttukeylem7  8898  axdclem2  8903  brdom3  8909  brdom7disj  8912  brdom6disj  8913  alephval2  8950  inar1  9156  axgroth6  9209  pinq  9308  nqereu  9310  prlem934  9414  supexpr  9435  supsrlem  9491  axpre-sup  9549  dedekind  9747  dedekindle  9748  fimaxre2  10498  lbreu  10500  sup2  10506  infm3  10509  supmul1  10515  supmullem2  10517  supmul  10518  infmrcl  10529  nnsub  10581  uzwo  11155  uzwoOLD  11156  nnwof  11159  uzinfmi  11172  ublbneg  11177  lbzbi  11181  zsupss  11182  uzsupss  11185  uzwo3  11188  zmax  11190  rpnnen1lem1  11219  rpnnen1lem2  11220  rpnnen1lem3  11221  rpnnen1lem4  11222  rpnnen1lem5  11223  xrsupsslem  11509  xrinfmsslem  11510  xrsupss  11511  xrinfmss  11512  iccsupr  11628  supicc  11679  supiccub  11680  supicclub  11681  flval2  11932  flval3  11933  fsequb  12067  axdc4uzlem  12074  ssnn0fi  12076  fsuppmapnn0fiubex  12080  faclbnd4lem4  12356  bccl  12382  hashgt12el  12463  hashbc  12484  hashge2el2dif  12503  wrdind  12684  wrd2ind  12685  sqrlem3  13060  rexanre  13161  rexico  13168  cau4  13171  caubnd2  13172  caubnd  13173  clim  13299  rlim  13300  rlim2  13301  rlim2lt  13302  rlim3  13303  clim2  13309  clim2c  13310  clim0c  13312  rlim0  13313  rlim0lt  13314  ello12r  13322  ello1d  13328  lo1bdd2  13329  lo1bddrp  13330  elo12r  13333  rlimconst  13349  rlimresb  13370  rlimcld2  13383  climabs0  13390  rlimcn2  13395  reccn2  13401  cn1lem  13402  rlimo1  13421  o1rlimmul  13423  lo1add  13431  lo1mul  13432  isercoll  13472  caucvgrlem  13477  incexclem  13630  climcnds  13645  divrcnv  13646  ruclem12  13956  sqrt2irr  13964  gcdcllem1  14131  gcdcllem2  14132  maxprmfct  14236  reumodprminv  14311  pc2dvds  14384  pcz  14386  prmpwdvds  14404  infpn2  14413  prmreclem1  14416  prmreclem2  14417  prmreclem3  14418  prmreclem5  14420  prmreclem6  14421  vdwlem6  14486  vdwlem8  14488  vdwlem13  14493  vdwnnlem1  14495  vdwnn  14498  ramz  14525  ramcl  14529  cshwrepswhash1  14569  prdsleval  14856  imasval  14890  imasaddfnlem  14907  imasvscafn  14916  mrisval  15009  isacs  15030  isacs2  15032  isacs1i  15036  mreacs  15037  acsfn  15038  acsfn2  15042  iscatd  15052  catidex  15053  catideu  15054  cidval  15056  catidd  15059  comfeq  15083  catpropd  15086  ismon  15110  isfunc  15212  isnat  15295  isprs  15538  drsdirfi  15546  ispos  15555  lubfval  15587  lubeldm  15590  lubval  15593  lubprop  15595  lublecllem  15597  glbfval  15600  glbeldm  15603  glbval  15606  glbprop  15608  joinval2lem  15617  joinlem  15620  meetval2lem  15631  meetlem  15634  isglbd  15726  lubl  15729  lubun  15732  clatleglb  15735  poslubmo  15755  posglbmo  15756  poslubd  15757  ipodrsima  15774  isdlat  15802  mgm1  15863  mgmidmo  15865  ismgmid  15870  ismgmid2  15873  mgmidsssn0  15875  gsumvalx  15876  gsumress  15882  gsumval2  15886  sgrp1  15897  mndclOLD  15910  mndassOLD  15911  ismndd  15922  mnd1  15940  mnd1OLD  15941  mhmima  15973  mrcmndind  15976  gsumvallem2  15982  gsumwspan  15993  sgrp2rid2  16023  sgrp2rid2ex  16024  sgrp2nmndlem4  16025  isgrpinv  16079  mhmmnd  16171  issubg4  16199  0subg  16205  cycsubgcl  16206  isnsg2  16210  nsgacs  16216  elnmz  16219  ghmrn  16259  ghmnsgima  16269  isga  16308  orbsta  16330  cntzfval  16337  elcntz  16339  resscntz  16348  oppgsubg  16377  symgextfo  16426  gsmsymgreqlem2  16435  gsmsymgreq  16436  pmtrdifel  16484  pmtrdifwrdellem3  16487  pmtrdifwrdel2  16490  psgnunilem2  16499  psgnunilem3  16500  odeq  16553  gexid  16580  gexlem2  16581  gexdvds  16583  isslw  16607  pgpssslw  16613  sylow2alem1  16616  sylow2alem2  16617  efgval  16714  efgrelexlemb  16747  efgcpbllemb  16752  gexex  16838  abl1  16851  dmdprd  17008  dprd2da  17070  pgpfac1lem5  17109  ring1  17227  isabv  17447  islss  17560  lssacs  17592  reslmhm  17677  islbs  17701  pj1lmhm  17725  lbsacsbs  17781  isrrg  17915  opsrval  18118  ply1coe  18316  cply1coe0bi  18321  zringlpir  18490  zlpir  18495  psgndiflemA  18615  ocvfval  18675  elocv  18677  iunocv  18690  frlmlbs  18809  islindf  18825  islinds2  18826  islindf2  18827  lindfrn  18834  lsslindf  18843  islindf4  18851  mat0dimcrng  18950  mdetunilem1  19092  mdetunilem9  19100  cpmat  19188  cpmatel  19190  1elcpmat  19194  m2cpminvid2lem  19233  chfacffsupp  19335  chfacfscmulfsupp  19338  chfacfpmmulfsupp  19342  basgen2  19469  bastop1  19473  isclo  19566  ordtbaslem  19667  iscn  19714  cnpval  19715  iscnp  19716  iscnp3  19723  lmbr  19737  lmbr2  19738  lmbrf  19739  cnprest  19768  cnprest2  19769  t0sep  19803  isreg  19811  t1sep2  19848  tgcmp  19879  1stcclb  19923  1stcfb  19924  2ndc1stc  19930  1stcrest  19932  2ndcdisj  19935  islly  19947  isnlly  19948  lly1stc  19975  isref  19988  islocfin  19996  elkgen  20015  kgencn  20035  elpt  20051  elptr  20052  ptcnplem  20100  tx1stc  20129  cnmpt21  20150  kqt0lem  20215  isr0  20216  regr1lem2  20219  r0sep  20227  nrmr0reg  20228  flffbas  20474  cnflf  20481  cnflf2  20482  lmflf  20484  txflf  20485  fclsopni  20494  fclsnei  20498  fclsrest  20503  fcfnei  20514  cnfcf  20521  alexsubb  20524  alexsubALTlem3  20527  qustgplem  20597  tsmsfbas  20604  tsmsgsum  20615  tsmsgsumOLD  20618  tsmsresOLD  20623  tsmsres  20624  tsmsf1o  20625  tsmsxplem1  20633  tsmsxp  20635  ustval  20683  isust  20684  ustincl  20688  ustdiag  20689  ustinvel  20690  ustexhalf  20691  ust0  20700  utopval  20713  ucnval  20758  isucn  20759  isucn2  20760  ucnima  20762  iscfilu  20769  ispsmet  20786  ismet  20804  isxmet  20805  imasdsf1olem  20854  imasf1oxmet  20856  imasf1omet  20857  metss  20989  met1stc  21002  prdsxmslem2  21010  metcnpi3  21027  txmetcnp  21028  metucnOLD  21069  metucn  21070  nlmvscn  21174  nrginvrcnlem  21177  nmoval  21200  nmolb  21202  nghmcn  21230  qtopbaslem  21243  icccmplem2  21306  icccmplem3  21307  reconnlem2  21310  metdscn  21338  cncfval  21370  elcncf2  21372  elcncf1di  21377  mulc1cncf  21387  cncfmet  21390  cnllycmp  21434  evth  21437  lebnumlem3  21441  lebnum  21442  xlebnum  21443  ishtpy  21450  isphtpy  21459  pi1xfr  21533  pi1coghm  21539  ipcn  21664  lmmbr2  21676  lmmbr3  21677  lmmbrf  21679  cfilfval  21681  iscfil  21682  fmcfil  21689  caufval  21692  iscau  21693  iscau2  21694  iscau3  21695  iscau4  21696  iscauf  21697  caucfil  21700  cfilresi  21712  causs  21715  lmclim  21719  cncmet  21739  cmetcusp1OLD  21769  cmetcusp1  21770  minveclem4c  21818  minveclem2  21819  minveclem3b  21821  minveclem4  21825  minveclem6  21827  minveclem7  21828  ivthlem2  21842  ivthlem3  21843  cniccbdd  21851  ovolunlem1  21886  ovoliunlem1  21891  ovoliun2  21895  ovolicc2lem3  21908  ismbl  21915  ioombl1lem4  21949  uniioombllem2  21970  uniioombllem6  21975  dyadmax  21985  dyadmbllem  21986  dyadmbl  21987  opnmbllem  21988  volcn  21993  ismbf1  22011  ismbf  22015  mbfeqalem  22027  mbfinf  22050  mbflimsup  22051  itg1climres  22099  mbfi1fseqlem6  22105  mbfi1flimlem  22107  itg2seq  22127  itg2monolem1  22135  itg2i1fseq  22140  itg2i1fseq2  22141  itg2cnlem1  22146  itg2cnlem2  22147  isibl  22150  dveflem  22358  ply1divex  22515  fta1g  22546  plyeq0lem  22585  dgrco  22650  plydivex  22671  fta1  22682  vieta1  22686  aannenlem1  22702  aannenlem2  22703  aalioulem2  22707  aalioulem3  22708  ulmval  22753  ulm2  22758  ulmi  22759  ulmres  22761  ulmshftlem  22762  ulmcaulem  22767  ulmcau  22768  ulmss  22770  ulmbdd  22771  ulmdvlem1  22773  ulmdvlem3  22775  mtestbdd  22778  iblulm  22780  abelthlem8  22812  pilem2  22825  pilem3  22826  divlogrlim  22994  cxpcn3  23100  dmarea  23265  rlimcnp  23273  cxplim  23279  cxploglim  23285  scvxcvx  23293  emcllem6  23308  ftalem1  23324  ftalem2  23325  ftalem3  23326  isppw2  23367  perfectlem2  23483  2sqlem6  23622  2sqlem10  23627  dchrisumlema  23651  dchrisumlem2  23653  dchrisumlem3  23654  dchrisum0  23683  pntpbnd  23751  pntibndlem3  23755  pntibnd  23756  pntleme  23771  pntlem3  23772  pntlemp  23773  pnt3  23775  istrkgld  23835  axtg5seg  23840  perpln1  24065  perpln2  24066  isperp  24067  brbtwn2  24186  colinearalg  24191  axsegconlem1  24198  axsegcon  24208  ax5seglem4  24213  ax5seglem5  24214  axlowdim  24242  axeuclidlem  24243  axcontlem1  24245  axcontlem2  24246  axcontlem4  24248  axcontlem5  24249  axcontlem8  24252  axcontlem12  24256  cusgra3v  24442  wlks  24497  wlkcompim  24504  wlkelwrd  24508  wlkntrllem3  24541  constr3trllem2  24629  1conngra  24653  wwlk  24659  clwwlk  24744  isrgrac  24912  rusgra0edg  24933  iseupa  24943  frgrawopreg1  25028  frgrawopreg2  25029  frgrareg  25095  frgraregord013  25096  isgrpo  25176  isgrpo2  25177  isgrpoi  25178  grpoideu  25189  grpoidinv2  25198  isgrp2d  25215  isgrpda  25277  exidu1  25306  cmpidelt  25309  cnid  25331  mulid  25336  ghgrpOLD  25348  isrngod  25359  rngoideu  25364  cnrngo  25383  vci  25419  isvclem  25448  isnvlem  25481  nvi  25485  nmcvcn  25583  lnoval  25645  islno  25646  isblo3i  25694  blo3i  25695  blocnilem  25697  blocni  25698  ajfval  25702  ubthlem1  25764  ubthlem2  25765  ubthlem3  25766  ubth  25767  minvecolem2  25769  minvecolem3  25770  minvecolem4c  25773  minvecolem4  25774  minvecolem5  25775  minvecolem6  25776  minvecolem7  25777  htthlem  25812  h2hcau  25874  h2hlm  25875  hilid  26056  hcau  26079  hlimi  26083  hlim2  26087  ocel  26177  adjsym  26730  ellnop  26755  ellnfn  26780  hhcno  26801  hhcnf  26802  0cnop  26876  0cnfn  26877  idcnop  26878  lnopeq  26906  elunop2  26910  lnophm  26916  lnconi  26930  lnopcnbd  26933  lnfncnbd  26954  imaelshi  26955  riesz3i  26959  riesz4i  26960  riesz4  26961  riesz1  26962  cnlnadjlem2  26965  cnlnadjlem5  26968  cnlnadjlem8  26971  cnlnadji  26973  nmopadjlei  26985  cnvbraval  27007  leopg  27019  leoppos  27023  mdbr  27191  dmdbr  27196  cdj3i  27338  rmoeq  27364  disjunsn  27431  funcnv5mpt  27489  fgreu  27491  fcnvgreu  27492  xrge0infss  27558  resspos  27625  isomnd  27669  inftmrel  27702  isinftm  27703  archiabl  27720  rngurd  27756  isarchiofld  27785  crefeq  27826  rge0scvg  27909  qqhcn  27950  esumpcvgval  28062  sigaval  28088  issgon  28101  isrnmeas  28149  ismbfm  28201  isanmbfm  28205  mbfmcst  28208  sitgval  28252  oddpwdc  28271  eulerpartlemd  28283  ballotleme  28413  signsw0g  28491  signswmnd  28492  lgamgulmlem2  28550  lgamgulmlem3  28551  lgamgulmlem5  28553  lgambdd  28557  lgamcvglem  28560  derangenlem  28593  subfacp1lem3  28604  subfacp1lem5  28606  subfacp1lem6  28607  subfacp1  28608  erdszelem8  28620  kur14  28638  cnpcon  28653  rescon  28669  cvmscbv  28681  iscvm  28682  cvmsi  28688  cvmsval  28689  cvmlift3lem2  28743  snmlval  28754  mclsssvlem  28900  mclsval  28901  mclsax  28907  mclsind  28908  ghomgrpilem1  29003  dfpo2  29160  dfon2lem9  29199  dfrdg2  29204  dfrdg3  29205  poseq  29309  soseq  29310  wrecseq123  29313  wfrlem1  29319  wfrlem15  29333  frrlem1  29363  sltval  29383  nocvxminlem  29426  nobndlem2  29429  nobndlem8  29435  nobndup  29436  nobnddown  29437  fin2so  30016  supaddc  30017  supadd  30018  heicant  30025  mblfinlem1  30027  mblfinlem2  30028  mblfinlem3  30029  ismblfin  30031  voliunnfl  30034  volsupnfl  30035  mbfresfi  30037  itg2addnc  30045  ftc1anc  30074  nn0prpwlem  30116  isfne  30133  isfne4  30134  isfne2  30136  isfne3  30137  neibastop3  30156  topmeet  30158  topjoin  30159  filnetlem4  30175  f1opr  30191  upixp  30196  indexdom  30201  filbcmb  30207  sdclem2  30211  fdc  30214  lmclim2  30227  caures  30229  istotbnd  30241  istotbnd3  30243  sstotbnd  30247  isbnd  30252  heibor  30293  bfp  30296  rrncmslem  30304  exidres  30316  exidresid  30317  idlval  30386  isidl  30387  0idl  30398  unichnidl  30404  pridl  30410  ismaxidl  30413  smprngopr  30425  igenval2  30439  prnc  30440  ispridlc  30443  scottexf  30552  scott0f  30553  isnacs  30612  isnacs2  30614  nacsfix  30620  mzpclval  30633  elmzpcl  30634  rencldnfilem  30730  infmrgelbi  30790  pellfundre  30793  pellfundlb  30796  wepwsolem  30963  fnwe2lem2  30973  aomclem8  30983  dfac11  30984  gicabl  31023  islnr3  31040  hbtlem2  31049  hbtlem5  31053  evth2f  31344  ubelsupr  31349  evthf  31356  fnchoice  31358  dstregt0  31417  upbdrech2  31462  mccl  31560  mullimc  31576  ellimcabssub0  31577  limcdm0  31578  climf  31582  mullimcf  31583  constlimc  31584  idlimc  31586  clim2f  31596  limsupre  31601  limcleqr  31604  addlimc  31608  0ellimcdiv  31609  clim2cf  31610  clim0cf  31614  cncfshift  31630  cncfperiod  31635  fperdvper  31669  dvdivbd  31674  dvbdfbdioo  31681  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvnprodlem3  31699  stoweidlem5  31741  stoweidlem9  31745  stoweidlem15  31751  stoweidlem16  31752  stoweidlem27  31763  stoweidlem28  31764  stoweidlem31  31767  stoweidlem34  31770  stoweidlem37  31773  stoweidlem46  31782  stoweidlem48  31784  stoweidlem51  31787  stoweidlem52  31788  stoweidlem59  31795  wallispilem3  31803  stirlinglem13  31822  fourierdlem2  31845  fourierdlem3  31846  fourierdlem16  31859  fourierdlem20  31863  fourierdlem21  31864  fourierdlem22  31865  fourierdlem25  31868  fourierdlem39  31882  fourierdlem42  31885  fourierdlem54  31897  fourierdlem64  31907  fourierdlem77  31920  fourierdlem83  31926  fourierdlem87  31930  fourierdlem103  31946  fourierdlem104  31947  etransclem48  32019  cbvral2  32131  raaan2  32134  2reu4a  32148  dfdfat2  32170  mgmhmima  32444  rnghmval  32532  lidlmsgrp  32559  lidlrng  32560  zlidlring  32561  uzlidlring  32562  2zrngamnd  32574  ply1mulgsumlem1  32856  ply1mulgsumlem2  32857  linindslinci  32919  lindslinindsimp1  32928  lindslinindsimp2lem5  32933  lindslinindsimp2  32934  linds0  32936  lindsrng01  32939  snlindsntor  32942  lmod1  32963  ldepsnlinc  32979  bnj1185  33720  bnj1385  33759  bnj66  33786  bnj106  33794  bnj155  33805  bnj852  33847  bnj893  33854  bnj1228  33935  bnj1234  33937  bnj1463  33979  riotasvd  34562  islfl  34660  eqlkr  34699  eqlkr3  34701  glbconN  34976  hlsuprexch  34980  ispsubsp  35344  ldilset  35708  isldil  35709  dilsetN  35753  isdilN  35754  trlset  35761  trlval  35762  cdleme27b  35969  cdleme29b  35976  cdleme31so  35980  cdleme31sn1  35982  cdleme31sn1c  35989  cdleme31fv  35991  cdleme40v  36070  istendo  36361  cdlemkid3N  36534  cdlemkid4  36535  cdlemkid5  36536  dihfval  36833  dihval  36834  islpolN  37085  hdmapffval  37431  hdmapfval  37432  hdmapval  37433  hdmapval2lem  37436  hgmapffval  37490  hgmapfval  37491  hgmapval  37492  hgmapvs  37496  taupilemrplb  37570  fiinfi  37596  imo72b2lem0  37786  imo72b2lem2  37788  imo72b2lem1  37792  imo72b2  37797