Theorem ralbidv 2839

Description: Formula-building rule for restricted universal quantifier (deduction rule). Revised to reduce dependecies on axioms. (Contributed by NM, 20-Nov-1994.) (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 2837	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1758   A.wral 2795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671

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

This theorem is referenced by:  ralbiiOLD  2846  2ralbidv  2861  rexralbidv  2863  raleqbi1dv  3021  raleqbidv  3027  cbvral2v  3051  rspc2  3175  rspc3v  3179  reu6i  3247  reu7  3251  sbcralt  3365  raaan  3885  raaanv  3886  r19.12sn  4039  2ralunsn  4178  elintg  4234  elintrabg  4239  eliin  4274  disjprg  4386  disjxun  4388  reusv2lem2  4592  reusv3  4598  reusv6OLD  4601  poeq1  4742  somo  4773  frirr  4795  fr2nr  4796  frminex  4798  wereu2  4815  posn  5005  frsn  5007  ralxpf  5084  cnvpo  5473  fnmptfvd  5905  iinpreima  5932  dff4  5956  dff13f  6072  eusvobj2  6183  ofreq  6423  sorpssuni  6469  sorpssint  6470  fr3nr  6491  onssmin  6508  funcnvuni  6630  f1oweALT  6661  frxp  6782  smoeq  6911  recseq  6933  tfrlem12  6948  tz7.48lem  6996  elixp2  7367  undifixp  7399  xpf1o  7573  nneneq  7594  ac6sfi  7657  frfi  7658  fipreima  7718  indexfi  7720  marypha1lem  7784  marypha1  7785  supeq1  7796  supeq3  7800  supmo  7803  eqsup  7807  supub  7810  suplub  7811  supmaxlem  7815  supisoex  7822  oieq1  7827  ordtypecbv  7832  ordtypelem3  7835  ordtypelem6  7838  ordtypelem7  7839  ordtypelem9  7841  wemaplem1  7861  wemaplem2  7862  zfregcl  7910  oemapval  7992  oemapvali  7993  cantnf  8002  cantnfOLD  8024  wemapwe  8029  wemapweOLD  8030  rankval3b  8134  unbndrank  8150  rankunb  8158  rankuni2b  8161  tcrank  8192  scottex  8193  scottexs  8195  scott0s  8196  bnd2  8201  dfac8clem  8303  ac5num  8307  acni  8316  acni2  8317  alephval3  8381  dfac4  8393  dfac5lem5  8398  dfac5  8399  dfac2a  8400  dfac2  8401  dfacacn  8411  kmlem2  8421  kmlem13  8432  cflem  8516  cflecard  8523  cfeq0  8526  cfsuc  8527  cfflb  8529  cofsmo  8539  cfsmolem  8540  cfcoflem  8542  coftr  8543  alephsing  8546  fin23lem11  8587  isfin3ds  8599  fin23lem17  8608  fin23lem39  8620  isf33lem  8636  isf34lem6  8650  fin1a2lem13  8682  hsmexlem4  8699  hsmex  8702  axcc2lem  8706  axcc3  8708  dcomex  8717  axdc2lem  8718  axdc3lem2  8721  axdc3lem3  8722  axdc3  8724  axdc4lem  8725  axcclem  8727  zorn2lem2  8767  zorn2lem7  8772  zorn2g  8773  zornn0g  8775  ttukeylem7  8785  axdclem2  8790  brdom3  8796  brdom7disj  8799  brdom6disj  8800  alephval2  8837  inar1  9043  axgroth6  9096  pinq  9197  nqereu  9199  prlem934  9303  supexpr  9324  supsrlem  9379  axpre-sup  9437  dedekind  9634  dedekindle  9635  fimaxre2  10379  lbreu  10381  sup2  10387  infm3  10390  supmul1  10396  supmullem2  10398  supmul  10399  infmrcl  10410  nnsub  10461  uzwo  11018  uzwoOLD  11019  nnwof  11022  uzinfmi  11035  ublbneg  11040  lbzbi  11044  zsupss  11045  uzsupss  11048  uzwo3  11049  zmax  11051  rpnnen1lem1  11080  rpnnen1lem2  11081  rpnnen1lem3  11082  rpnnen1lem4  11083  rpnnen1lem5  11084  xrsupsslem  11370  xrinfmsslem  11371  xrsupss  11372  xrinfmss  11373  iccsupr  11483  supicc  11534  supiccub  11535  supicclub  11536  flval2  11763  flval3  11764  fsequb  11898  axdc4uzlem  11905  faclbnd4lem4  12173  bccl  12199  hashgt12el  12275  hashge2el2dif  12286  hashbc  12308  wrdind  12473  wrd2ind  12474  sqrlem3  12836  rexanre  12936  rexico  12943  cau4  12946  caubnd2  12947  caubnd  12948  clim  13074  rlim  13075  rlim2  13076  rlim2lt  13077  rlim3  13078  clim2  13084  clim2c  13085  clim0c  13087  rlim0  13088  rlim0lt  13089  ello12r  13097  ello1d  13103  lo1bdd2  13104  lo1bddrp  13105  elo12r  13108  rlimconst  13124  rlimresb  13145  rlimcld2  13158  climabs0  13165  rlimcn2  13170  reccn2  13176  cn1lem  13177  rlimo1  13196  o1rlimmul  13198  lo1add  13206  lo1mul  13207  isercoll  13247  caucvgrlem  13252  incexclem  13401  climcnds  13416  divrcnv  13417  ruclem12  13625  sqr2irr  13633  gcdcllem1  13797  gcdcllem2  13798  maxprmfct  13901  reumodprminv  13974  pc2dvds  14047  pcz  14049  prmpwdvds  14067  infpn2  14076  prmreclem1  14079  prmreclem2  14080  prmreclem3  14081  prmreclem5  14083  prmreclem6  14084  vdwlem6  14149  vdwlem8  14151  vdwlem13  14156  vdwnnlem1  14158  vdwnn  14161  ramz  14188  ramcl  14192  cshwrepswhash1  14231  prdsleval  14517  imasval  14551  imasaddfnlem  14568  imasvscafn  14577  mrisval  14670  isacs  14691  isacs2  14693  isacs1i  14697  mreacs  14698  acsfn  14699  acsfn2  14703  iscatd  14713  catidex  14714  catideu  14715  cidval  14717  catidd  14720  comfeq  14747  catpropd  14750  ismon  14774  isfunc  14876  isnat  14959  isprs  15202  drsdirfi  15210  ispos  15219  lubfval  15250  lubeldm  15253  lubval  15256  lubprop  15258  lublecllem  15260  glbfval  15263  glbeldm  15266  glbval  15269  glbprop  15271  joinval2lem  15280  joinlem  15283  meetval2lem  15294  meetlem  15297  isglbd  15389  lubl  15392  lubun  15395  clatleglb  15398  poslubmo  15418  posglbmo  15419  poslubd  15420  ipodrsima  15437  isdlat  15465  mgmidmo  15520  ismgmid  15537  ismgmid2  15540  ismndd  15546  mhmima  15593  mrcmndind  15596  gsumvallem1  15602  gsumvallem2  15603  gsumvalx  15604  gsumress  15609  gsumval2  15615  gsumwspan  15626  isgrpinv  15690  issubg4  15802  0subg  15808  cycsubgcl  15809  isnsg2  15813  nsgacs  15819  elnmz  15822  ghmrn  15862  ghmnsgima  15872  isga  15911  orbsta  15933  cntzfval  15940  elcntz  15942  resscntz  15951  oppgsubg  15980  symgextfo  16029  gsmsymgreqlem2  16038  gsmsymgreq  16039  pmtrdifel  16088  pmtrdifwrdellem3  16091  pmtrdifwrdel  16093  pmtrdifwrdel2  16094  psgnunilem2  16103  psgnunilem3  16104  odeq  16157  gexid  16184  gexlem2  16185  gexdvds  16187  isslw  16211  pgpssslw  16217  sylow2alem1  16220  sylow2alem2  16221  efgval  16318  efgrelexlemb  16351  efgcpbllemb  16356  gexex  16439  dmdprd  16585  dprd2da  16646  pgpfac1lem5  16685  isabv  17010  islss  17122  lssacs  17154  reslmhm  17239  islbs  17263  pj1lmhm  17287  lbsacsbs  17343  isrrg  17465  opsrval  17663  ply1coe  17855  zringlpir  18015  zlpir  18020  psgndiflemA  18140  ocvfval  18200  elocv  18202  iunocv  18215  frlmlbs  18334  islindf  18350  islinds2  18351  islindf2  18352  lindfrn  18359  lsslindf  18368  islindf4  18376  mdetunilem1  18534  mdetunilem9  18542  basgen2  18710  bastop1  18714  isclo  18807  ordtbaslem  18908  iscn  18955  cnpval  18956  iscnp  18957  iscnp3  18964  lmbr  18978  lmbr2  18979  lmbrf  18980  cnprest  19009  cnprest2  19010  t0sep  19044  isreg  19052  t1sep2  19089  tgcmp  19120  1stcclb  19164  1stcfb  19165  2ndc1stc  19171  1stcrest  19173  2ndcdisj  19176  islly  19188  isnlly  19189  lly1stc  19216  elkgen  19225  kgencn  19245  elpt  19261  elptr  19262  ptcnplem  19310  tx1stc  19339  cnmpt21  19360  kqt0lem  19425  isr0  19426  regr1lem2  19429  r0sep  19437  nrmr0reg  19438  flffbas  19684  cnflf  19691  cnflf2  19692  lmflf  19694  txflf  19695  fclsopni  19704  fclsnei  19708  fclsrest  19713  fcfnei  19724  cnfcf  19731  alexsubb  19734  alexsubALTlem3  19737  divstgplem  19807  tsmsfbas  19814  tsmsgsum  19825  tsmsgsumOLD  19828  tsmsresOLD  19833  tsmsres  19834  tsmsf1o  19835  tsmsxplem1  19843  tsmsxp  19845  ustval  19893  isust  19894  ustincl  19898  ustdiag  19899  ustinvel  19900  ustexhalf  19901  ust0  19910  utopval  19923  ucnval  19968  isucn  19969  isucn2  19970  ucnima  19972  iscfilu  19979  ispsmet  19996  ismet  20014  isxmet  20015  imasdsf1olem  20064  imasf1oxmet  20066  imasf1omet  20067  metss  20199  met1stc  20212  prdsxmslem2  20220  metcnpi3  20237  txmetcnp  20238  metucnOLD  20279  metucn  20280  nlmvscn  20384  nrginvrcnlem  20387  nmoval  20410  nmolb  20412  nghmcn  20440  qtopbaslem  20453  icccmplem2  20516  icccmplem3  20517  reconnlem2  20520  metdscn  20548  cncfval  20580  elcncf2  20582  elcncf1di  20587  mulc1cncf  20597  cncfmet  20600  cnllycmp  20644  evth  20647  lebnumlem3  20651  lebnum  20652  xlebnum  20653  ishtpy  20660  isphtpy  20669  pi1xfr  20743  pi1coghm  20749  ipcn  20874  lmmbr2  20886  lmmbr3  20887  lmmbrf  20889  cfilfval  20891  iscfil  20892  fmcfil  20899  caufval  20902  iscau  20903  iscau2  20904  iscau3  20905  iscau4  20906  iscauf  20907  caucfil  20910  cfilresi  20922  causs  20925  lmclim  20929  cncmet  20949  cmetcusp1OLD  20979  cmetcusp1  20980  minveclem4c  21028  minveclem2  21029  minveclem3b  21031  minveclem4  21035  minveclem6  21037  minveclem7  21038  ivthlem2  21052  ivthlem3  21053  cniccbdd  21061  ovolunlem1  21096  ovoliunlem1  21101  ovoliun2  21105  ovolicc2lem3  21118  ismbl  21125  ioombl1lem4  21158  uniioombllem2  21179  uniioombllem6  21184  dyadmax  21194  dyadmbllem  21195  dyadmbl  21196  opnmbllem  21197  volcn  21202  ismbf1  21220  ismbf  21224  mbfeqalem  21236  mbfinf  21259  mbflimsup  21260  itg1climres  21308  mbfi1fseqlem6  21314  mbfi1flimlem  21316  itg2seq  21336  itg2monolem1  21344  itg2i1fseq  21349  itg2i1fseq2  21350  itg2cnlem1  21355  itg2cnlem2  21356  isibl  21359  dveflem  21567  ply1divex  21724  fta1g  21755  plyeq0lem  21794  dgrco  21858  plydivex  21879  fta1  21890  vieta1  21894  aannenlem1  21910  aannenlem2  21911  aalioulem2  21915  aalioulem3  21916  ulmval  21961  ulm2  21966  ulmi  21967  ulmres  21969  ulmshftlem  21970  ulmcaulem  21975  ulmcau  21976  ulmss  21978  ulmbdd  21979  ulmdvlem1  21981  ulmdvlem3  21983  mtestbdd  21986  iblulm  21988  abelthlem8  22020  pilem2  22033  pilem3  22034  divlogrlim  22196  cxpcn3  22302  dmarea  22467  rlimcnp  22475  cxplim  22481  cxploglim  22487  scvxcvx  22495  emcllem6  22510  ftalem1  22526  ftalem2  22527  ftalem3  22528  isppw2  22569  perfectlem2  22685  2sqlem6  22824  2sqlem10  22829  dchrisumlema  22853  dchrisumlem2  22855  dchrisumlem3  22856  dchrisum0  22885  pntpbnd  22953  pntibndlem3  22957  pntibnd  22958  pntleme  22973  pntlem3  22974  pntlemp  22975  pnt3  22977  istrkgld  23037  axtg5seg  23042  perpln1  23229  perpln2  23230  isperp  23231  brbtwn2  23286  colinearalg  23291  axsegconlem1  23298  axsegcon  23308  ax5seglem4  23313  ax5seglem5  23314  axlowdim  23342  axeuclidlem  23343  axcontlem1  23345  axcontlem2  23346  axcontlem4  23348  axcontlem5  23349  axcontlem8  23352  axcontlem12  23356  cusgra3v  23507  wlks  23560  wlkntrllem3  23595  constr3trllem2  23672  1conngra  23696  iseupa  23721  isgrpo  23818  isgrpo2  23819  isgrpoi  23820  grpoideu  23831  grpoidinv2  23840  isgrp2d  23857  isgrpda  23919  exidu1  23948  cmpidelt  23951  cnid  23973  mulid  23978  ghgrp  23990  isrngod  24001  rngoideu  24006  cnrngo  24025  vci  24061  isvclem  24090  isnvlem  24123  nvi  24127  nmcvcn  24225  lnoval  24287  islno  24288  isblo3i  24336  blo3i  24337  blocnilem  24339  blocni  24340  ajfval  24344  ubthlem1  24406  ubthlem2  24407  ubthlem3  24408  ubth  24409  minvecolem2  24411  minvecolem3  24412  minvecolem4c  24415  minvecolem4  24416  minvecolem5  24417  minvecolem6  24418  minvecolem7  24419  htthlem  24454  h2hcau  24516  h2hlm  24517  hilid  24698  hcau  24721  hlimi  24725  hlim2  24729  ocel  24819  adjsym  25372  ellnop  25397  ellnfn  25422  hhcno  25443  hhcnf  25444  0cnop  25518  0cnfn  25519  idcnop  25520  lnopeq  25548  elunop2  25552  lnophm  25558  lnconi  25572  lnopcnbd  25575  lnfncnbd  25596  imaelshi  25597  riesz3i  25601  riesz4i  25602  riesz4  25603  riesz1  25604  cnlnadjlem2  25607  cnlnadjlem5  25610  cnlnadjlem8  25613  cnlnadji  25615  nmopadjlei  25627  cnvbraval  25649  leopg  25661  leoppos  25665  mdbr  25833  dmdbr  25838  cdj3i  25980  rmoeq  26006  disjunsn  26070  funcnv5mpt  26122  fgreu  26124  xrge0infss  26187  resspos  26254  isomnd  26298  inftmrel  26331  isinftm  26332  archiabl  26349  rngurd  26390  isarchiofld  26419  rge0scvg  26513  qqhcn  26554  esumpcvgval  26661  sigaval  26687  issgon  26700  isrnmeas  26748  ismbfm  26801  isanmbfm  26805  mbfmcst  26808  sitgval  26852  oddpwdc  26871  eulerpartlemd  26883  ballotleme  27013  signsw0g  27091  signswmnd  27092  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamgulmlem5  27153  lgambdd  27157  lgamcvglem  27160  derangenlem  27193  subfacp1lem3  27204  subfacp1lem5  27206  subfacp1lem6  27207  subfacp1  27208  erdszelem8  27220  kur14  27238  cnpcon  27253  rescon  27269  cvmscbv  27281  iscvm  27282  cvmsi  27288  cvmsval  27289  cvmlift3lem2  27343  snmlval  27354  ghomgrpilem1  27438  dfpo2  27699  dfon2lem9  27738  dfrdg2  27743  dfrdg3  27744  poseq  27848  soseq  27849  wrecseq123  27852  wfrlem1  27858  wfrlem15  27872  frrlem1  27902  sltval  27922  nocvxminlem  27965  nobndlem2  27968  nobndlem8  27974  nobndup  27975  nobnddown  27976  fin2so  28554  supaddc  28555  supadd  28556  heicant  28564  mblfinlem1  28566  mblfinlem2  28567  mblfinlem3  28568  ismblfin  28570  voliunnfl  28573  volsupnfl  28574  mbfresfi  28576  itg2addnc  28584  ftc1anc  28613  nn0prpwlem  28655  isfne  28678  isfne4  28679  isfne2  28681  isfne3  28682  isref  28689  islocfin  28706  neibastop3  28721  topmeet  28723  topjoin  28724  filnetlem4  28740  f1opr  28756  upixp  28761  indexdom  28766  filbcmb  28772  sdclem2  28776  fdc  28779  lmclim2  28792  caures  28794  istotbnd  28806  istotbnd3  28808  sstotbnd  28812  isbnd  28817  heibor  28858  bfp  28861  rrncmslem  28869  exidres  28881  exidresid  28882  idlval  28951  isidl  28952  0idl  28963  unichnidl  28969  pridl  28975  ismaxidl  28978  smprngopr  28990  igenval2  29004  prnc  29005  ispridlc  29008  scottexf  29118  scott0f  29119  isnacs  29178  isnacs2  29180  nacsfix  29186  mzpclval  29199  elmzpcl  29200  rencldnfilem  29297  infmrgelbi  29357  pellfundre  29360  pellfundlb  29363  wepwsolem  29532  fnwe2lem2  29542  aomclem8  29552  dfac11  29553  gicabl  29592  islnr3  29609  hbtlem2  29618  hbtlem5  29622  evth2f  29875  ubelsupr  29880  evthf  29887  fnchoice  29889  stoweidlem5  29938  stoweidlem9  29942  stoweidlem15  29948  stoweidlem16  29949  stoweidlem27  29960  stoweidlem28  29961  stoweidlem31  29964  stoweidlem34  29967  stoweidlem37  29970  stoweidlem46  29979  stoweidlem48  29981  stoweidlem51  29984  stoweidlem52  29985  stoweidlem59  29992  wallispilem3  30000  stirlinglem13  30019  cbvral2  30134  raaan2  30137  2reu4a  30151  dfdfat2  30175  wlkelwrd  30418  wlkcompim  30425  wwlk  30453  clwwlk  30567  rusgra0edg  30711  frgrawopreg1  30781  frgrawopreg2  30782  frgrareg  30848  frgraregord013  30849  ssnn0fi  30884  fsuppmapnn0fiubex  30938  ply1mulgsumlem1  30986  ply1mulgsumlem2  30987  cply1coe0bi  30992  scmatscmidr  31012  mat0dimcrng  31020  dmatelnd  31029  dmatsubcl  31031  dmatmulcl  31033  scmatmulcl  31040  linindslinci  31089  lindslinindsimp1  31098  lindslinindsimp2lem5  31103  lindslinindsimp2  31104  linds0  31106  lindsrng01  31109  snlindsntor  31112  mnd1  31128  grp1  31129  abl1  31130  rng1  31132  lmod1  31141  ldepsnlinc  31157  cpmat  31172  cpmatel  31174  1elcpmat  31178  m2pminv2lem  31212  chfacffsupp  31310  chfacfscmulfsupp  31313  chfacfpmmulfsupp  31317  bnj1185  32087  bnj1385  32126  bnj66  32153  bnj106  32161  bnj155  32172  bnj852  32214  bnj893  32221  bnj1228  32302  bnj1234  32304  bnj1463  32346  riotasvd  32913  islfl  33011  eqlkr  33050  eqlkr3  33052  glbconN  33327  hlsuprexch  33331  ispsubsp  33695  ldilset  34059  isldil  34060  dilsetN  34103  isdilN  34104  trlset  34111  trlval  34112  cdleme27b  34318  cdleme29b  34325  cdleme31so  34329  cdleme31sn1  34331  cdleme31sn1c  34338  cdleme31fv  34340  cdleme40v  34419  istendo  34710  cdlemkid3N  34883  cdlemkid4  34884  cdlemkid5  34885  dihfval  35182  dihval  35183  islpolN  35434  hdmapffval  35780  hdmapfval  35781  hdmapval  35782  hdmapval2lem  35785  hgmapffval  35839  hgmapfval  35840  hgmapval  35841  hgmapvs  35845  taupilemrplb  35920