Theorem ralbidv 2903

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 2900	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1767   A.wral 2814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

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

This theorem is referenced by:  2ralbidv  2908  ralbiiOLD  2976  rexralbidv  2981  raleqbi1dv  3066  raleqbidv  3072  cbvral2v  3096  rspc2  3222  rspc3v  3226  reu6i  3294  reu7  3298  sbcralt  3412  raaan  3935  raaanv  3936  2ralsng  4064  r19.12sn  4093  2ralunsn  4234  elintg  4290  elintrabg  4295  eliin  4331  disjprg  4443  disjxun  4445  reusv2lem2  4649  reusv3  4655  reusv6OLD  4658  poeq1  4803  somo  4834  frirr  4856  fr2nr  4857  frminex  4859  wereu2  4876  posn  5067  frsn  5069  ralxpf  5147  cnvpo  5543  fnmptfvd  5982  iinpreima  6009  dff4  6033  dff13f  6153  eusvobj2  6275  ofreq  6525  sorpssuni  6571  sorpssint  6572  fr3nr  6593  onssmin  6610  funcnvuni  6734  f1oweALT  6765  frxp  6890  smoeq  7018  recseq  7040  tfrlem12  7055  tz7.48lem  7103  elixp2  7470  undifixp  7502  xpf1o  7676  nneneq  7697  ac6sfi  7760  frfi  7761  fipreima  7822  indexfi  7824  marypha1lem  7889  marypha1  7890  supeq1  7901  supeq3  7905  supmo  7908  eqsup  7912  supub  7915  suplub  7916  supmaxlem  7920  supisoex  7928  oieq1  7933  ordtypecbv  7938  ordtypelem3  7941  ordtypelem6  7944  ordtypelem7  7945  ordtypelem9  7947  wemaplem1  7967  wemaplem2  7968  zfregcl  8016  oemapval  8098  oemapvali  8099  cantnf  8108  cantnfOLD  8130  wemapwe  8135  wemapweOLD  8136  rankval3b  8240  unbndrank  8256  rankunb  8264  rankuni2b  8267  tcrank  8298  scottex  8299  scottexs  8301  scott0s  8302  bnd2  8307  dfac8clem  8409  ac5num  8413  acni  8422  acni2  8423  alephval3  8487  dfac4  8499  dfac5lem5  8504  dfac5  8505  dfac2a  8506  dfac2  8507  dfacacn  8517  kmlem2  8527  kmlem13  8538  cflem  8622  cflecard  8629  cfeq0  8632  cfsuc  8633  cfflb  8635  cofsmo  8645  cfsmolem  8646  cfcoflem  8648  coftr  8649  alephsing  8652  fin23lem11  8693  isfin3ds  8705  fin23lem17  8714  fin23lem39  8726  isf33lem  8742  isf34lem6  8756  fin1a2lem13  8788  hsmexlem4  8805  hsmex  8808  axcc2lem  8812  axcc3  8814  dcomex  8823  axdc2lem  8824  axdc3lem2  8827  axdc3lem3  8828  axdc3  8830  axdc4lem  8831  axcclem  8833  zorn2lem2  8873  zorn2lem7  8878  zorn2g  8879  zornn0g  8881  ttukeylem7  8891  axdclem2  8896  brdom3  8902  brdom7disj  8905  brdom6disj  8906  alephval2  8943  inar1  9149  axgroth6  9202  pinq  9301  nqereu  9303  prlem934  9407  supexpr  9428  supsrlem  9484  axpre-sup  9542  dedekind  9739  dedekindle  9740  fimaxre2  10487  lbreu  10489  sup2  10495  infm3  10498  supmul1  10504  supmullem2  10506  supmul  10507  infmrcl  10518  nnsub  10570  uzwo  11140  uzwoOLD  11141  nnwof  11144  uzinfmi  11157  ublbneg  11162  lbzbi  11166  zsupss  11167  uzsupss  11170  uzwo3  11173  zmax  11175  rpnnen1lem1  11204  rpnnen1lem2  11205  rpnnen1lem3  11206  rpnnen1lem4  11207  rpnnen1lem5  11208  xrsupsslem  11494  xrinfmsslem  11495  xrsupss  11496  xrinfmss  11497  iccsupr  11613  supicc  11664  supiccub  11665  supicclub  11666  flval2  11913  flval3  11914  fsequb  12048  axdc4uzlem  12055  ssnn0fi  12057  fsuppmapnn0fiubex  12061  faclbnd4lem4  12336  bccl  12362  hashgt12el  12440  hashbc  12462  hashge2el2dif  12481  wrdind  12659  wrd2ind  12660  sqrlem3  13035  rexanre  13135  rexico  13142  cau4  13145  caubnd2  13146  caubnd  13147  clim  13273  rlim  13274  rlim2  13275  rlim2lt  13276  rlim3  13277  clim2  13283  clim2c  13284  clim0c  13286  rlim0  13287  rlim0lt  13288  ello12r  13296  ello1d  13302  lo1bdd2  13303  lo1bddrp  13304  elo12r  13307  rlimconst  13323  rlimresb  13344  rlimcld2  13357  climabs0  13364  rlimcn2  13369  reccn2  13375  cn1lem  13376  rlimo1  13395  o1rlimmul  13397  lo1add  13405  lo1mul  13406  isercoll  13446  caucvgrlem  13451  incexclem  13604  climcnds  13619  divrcnv  13620  ruclem12  13828  sqrt2irr  13836  gcdcllem1  14001  gcdcllem2  14002  maxprmfct  14106  reumodprminv  14181  pc2dvds  14254  pcz  14256  prmpwdvds  14274  infpn2  14283  prmreclem1  14286  prmreclem2  14287  prmreclem3  14288  prmreclem5  14290  prmreclem6  14291  vdwlem6  14356  vdwlem8  14358  vdwlem13  14363  vdwnnlem1  14365  vdwnn  14368  ramz  14395  ramcl  14399  cshwrepswhash1  14438  prdsleval  14725  imasval  14759  imasaddfnlem  14776  imasvscafn  14785  mrisval  14878  isacs  14899  isacs2  14901  isacs1i  14905  mreacs  14906  acsfn  14907  acsfn2  14911  iscatd  14921  catidex  14922  catideu  14923  cidval  14925  catidd  14928  comfeq  14955  catpropd  14958  ismon  14982  isfunc  15084  isnat  15167  isprs  15410  drsdirfi  15418  ispos  15427  lubfval  15458  lubeldm  15461  lubval  15464  lubprop  15466  lublecllem  15468  glbfval  15471  glbeldm  15474  glbval  15477  glbprop  15479  joinval2lem  15488  joinlem  15491  meetval2lem  15502  meetlem  15505  isglbd  15597  lubl  15600  lubun  15603  clatleglb  15606  poslubmo  15626  posglbmo  15627  poslubd  15628  ipodrsima  15645  isdlat  15673  mgmidmo  15728  ismgmid  15745  ismgmid2  15748  ismndd  15754  mhmima  15801  mrcmndind  15804  gsumvallem1  15810  gsumvallem2  15811  gsumvalx  15812  gsumress  15817  gsumval2  15823  gsumwspan  15834  isgrpinv  15898  issubg4  16012  0subg  16018  cycsubgcl  16019  isnsg2  16023  nsgacs  16029  elnmz  16032  ghmrn  16072  ghmnsgima  16082  isga  16121  orbsta  16143  cntzfval  16150  elcntz  16152  resscntz  16161  oppgsubg  16190  symgextfo  16239  gsmsymgreqlem2  16248  gsmsymgreq  16249  pmtrdifel  16298  pmtrdifwrdellem3  16301  pmtrdifwrdel  16303  pmtrdifwrdel2  16304  psgnunilem2  16313  psgnunilem3  16314  odeq  16367  gexid  16394  gexlem2  16395  gexdvds  16397  isslw  16421  pgpssslw  16427  sylow2alem1  16430  sylow2alem2  16431  efgval  16528  efgrelexlemb  16561  efgcpbllemb  16566  gexex  16649  dmdprd  16817  dprd2da  16878  pgpfac1lem5  16917  isabv  17248  islss  17361  lssacs  17393  reslmhm  17478  islbs  17502  pj1lmhm  17526  lbsacsbs  17582  isrrg  17704  opsrval  17907  ply1coe  18105  cply1coe0bi  18110  zringlpir  18276  zlpir  18281  psgndiflemA  18401  ocvfval  18461  elocv  18463  iunocv  18476  frlmlbs  18595  islindf  18611  islinds2  18612  islindf2  18613  lindfrn  18620  lsslindf  18629  islindf4  18637  mat0dimcrng  18736  dmatmulcl  18766  mdetunilem1  18878  mdetunilem9  18886  cpmat  18974  cpmatel  18976  1elcpmat  18980  m2cpminvid2lem  19019  chfacffsupp  19121  chfacfscmulfsupp  19124  chfacfpmmulfsupp  19128  basgen2  19254  bastop1  19258  isclo  19351  ordtbaslem  19452  iscn  19499  cnpval  19500  iscnp  19501  iscnp3  19508  lmbr  19522  lmbr2  19523  lmbrf  19524  cnprest  19553  cnprest2  19554  t0sep  19588  isreg  19596  t1sep2  19633  tgcmp  19664  1stcclb  19708  1stcfb  19709  2ndc1stc  19715  1stcrest  19717  2ndcdisj  19720  islly  19732  isnlly  19733  lly1stc  19760  elkgen  19769  kgencn  19789  elpt  19805  elptr  19806  ptcnplem  19854  tx1stc  19883  cnmpt21  19904  kqt0lem  19969  isr0  19970  regr1lem2  19973  r0sep  19981  nrmr0reg  19982  flffbas  20228  cnflf  20235  cnflf2  20236  lmflf  20238  txflf  20239  fclsopni  20248  fclsnei  20252  fclsrest  20257  fcfnei  20268  cnfcf  20275  alexsubb  20278  alexsubALTlem3  20281  divstgplem  20351  tsmsfbas  20358  tsmsgsum  20369  tsmsgsumOLD  20372  tsmsresOLD  20377  tsmsres  20378  tsmsf1o  20379  tsmsxplem1  20387  tsmsxp  20389  ustval  20437  isust  20438  ustincl  20442  ustdiag  20443  ustinvel  20444  ustexhalf  20445  ust0  20454  utopval  20467  ucnval  20512  isucn  20513  isucn2  20514  ucnima  20516  iscfilu  20523  ispsmet  20540  ismet  20558  isxmet  20559  imasdsf1olem  20608  imasf1oxmet  20610  imasf1omet  20611  metss  20743  met1stc  20756  prdsxmslem2  20764  metcnpi3  20781  txmetcnp  20782  metucnOLD  20823  metucn  20824  nlmvscn  20928  nrginvrcnlem  20931  nmoval  20954  nmolb  20956  nghmcn  20984  qtopbaslem  20997  icccmplem2  21060  icccmplem3  21061  reconnlem2  21064  metdscn  21092  cncfval  21124  elcncf2  21126  elcncf1di  21131  mulc1cncf  21141  cncfmet  21144  cnllycmp  21188  evth  21191  lebnumlem3  21195  lebnum  21196  xlebnum  21197  ishtpy  21204  isphtpy  21213  pi1xfr  21287  pi1coghm  21293  ipcn  21418  lmmbr2  21430  lmmbr3  21431  lmmbrf  21433  cfilfval  21435  iscfil  21436  fmcfil  21443  caufval  21446  iscau  21447  iscau2  21448  iscau3  21449  iscau4  21450  iscauf  21451  caucfil  21454  cfilresi  21466  causs  21469  lmclim  21473  cncmet  21493  cmetcusp1OLD  21523  cmetcusp1  21524  minveclem4c  21572  minveclem2  21573  minveclem3b  21575  minveclem4  21579  minveclem6  21581  minveclem7  21582  ivthlem2  21596  ivthlem3  21597  cniccbdd  21605  ovolunlem1  21640  ovoliunlem1  21645  ovoliun2  21649  ovolicc2lem3  21662  ismbl  21669  ioombl1lem4  21703  uniioombllem2  21724  uniioombllem6  21729  dyadmax  21739  dyadmbllem  21740  dyadmbl  21741  opnmbllem  21742  volcn  21747  ismbf1  21765  ismbf  21769  mbfeqalem  21781  mbfinf  21804  mbflimsup  21805  itg1climres  21853  mbfi1fseqlem6  21859  mbfi1flimlem  21861  itg2seq  21881  itg2monolem1  21889  itg2i1fseq  21894  itg2i1fseq2  21895  itg2cnlem1  21900  itg2cnlem2  21901  isibl  21904  dveflem  22112  ply1divex  22269  fta1g  22300  plyeq0lem  22339  dgrco  22403  plydivex  22424  fta1  22435  vieta1  22439  aannenlem1  22455  aannenlem2  22456  aalioulem2  22460  aalioulem3  22461  ulmval  22506  ulm2  22511  ulmi  22512  ulmres  22514  ulmshftlem  22515  ulmcaulem  22520  ulmcau  22521  ulmss  22523  ulmbdd  22524  ulmdvlem1  22526  ulmdvlem3  22528  mtestbdd  22531  iblulm  22533  abelthlem8  22565  pilem2  22578  pilem3  22579  divlogrlim  22741  cxpcn3  22847  dmarea  23012  rlimcnp  23020  cxplim  23026  cxploglim  23032  scvxcvx  23040  emcllem6  23055  ftalem1  23071  ftalem2  23072  ftalem3  23073  isppw2  23114  perfectlem2  23230  2sqlem6  23369  2sqlem10  23374  dchrisumlema  23398  dchrisumlem2  23400  dchrisumlem3  23401  dchrisum0  23430  pntpbnd  23498  pntibndlem3  23502  pntibnd  23503  pntleme  23518  pntlem3  23519  pntlemp  23520  pnt3  23522  istrkgld  23582  axtg5seg  23587  isismt  23646  perpln1  23792  perpln2  23793  isperp  23794  brbtwn2  23881  colinearalg  23886  axsegconlem1  23893  axsegcon  23903  ax5seglem4  23908  ax5seglem5  23909  axlowdim  23937  axeuclidlem  23938  axcontlem1  23940  axcontlem2  23941  axcontlem4  23943  axcontlem5  23944  axcontlem8  23947  axcontlem12  23951  cusgra3v  24137  wlks  24192  wlkcompim  24199  wlkelwrd  24203  wlkntrllem3  24236  constr3trllem2  24324  1conngra  24348  wwlk  24354  clwwlk  24439  rusgra0edg  24628  iseupa  24638  frgrawopreg1  24724  frgrawopreg2  24725  frgrareg  24791  frgraregord013  24792  isgrpo  24871  isgrpo2  24872  isgrpoi  24873  grpoideu  24884  grpoidinv2  24893  isgrp2d  24910  isgrpda  24972  exidu1  25001  cmpidelt  25004  cnid  25026  mulid  25031  ghgrp  25043  isrngod  25054  rngoideu  25059  cnrngo  25078  vci  25114  isvclem  25143  isnvlem  25176  nvi  25180  nmcvcn  25278  lnoval  25340  islno  25341  isblo3i  25389  blo3i  25390  blocnilem  25392  blocni  25393  ajfval  25397  ubthlem1  25459  ubthlem2  25460  ubthlem3  25461  ubth  25462  minvecolem2  25464  minvecolem3  25465  minvecolem4c  25468  minvecolem4  25469  minvecolem5  25470  minvecolem6  25471  minvecolem7  25472  htthlem  25507  h2hcau  25569  h2hlm  25570  hilid  25751  hcau  25774  hlimi  25778  hlim2  25782  ocel  25872  adjsym  26425  ellnop  26450  ellnfn  26475  hhcno  26496  hhcnf  26497  0cnop  26571  0cnfn  26572  idcnop  26573  lnopeq  26601  elunop2  26605  lnophm  26611  lnconi  26625  lnopcnbd  26628  lnfncnbd  26649  imaelshi  26650  riesz3i  26654  riesz4i  26655  riesz4  26656  riesz1  26657  cnlnadjlem2  26660  cnlnadjlem5  26663  cnlnadjlem8  26666  cnlnadji  26668  nmopadjlei  26680  cnvbraval  26702  leopg  26714  leoppos  26718  mdbr  26886  dmdbr  26891  cdj3i  27033  rmoeq  27059  disjunsn  27123  funcnv5mpt  27180  fgreu  27182  xrge0infss  27245  resspos  27306  isomnd  27350  inftmrel  27383  isinftm  27384  archiabl  27401  rngurd  27438  isarchiofld  27467  rge0scvg  27564  qqhcn  27605  ismntop  27641  esumpcvgval  27721  sigaval  27747  issgon  27760  isrnmeas  27808  ismbfm  27860  isanmbfm  27864  mbfmcst  27867  sitgval  27911  oddpwdc  27930  eulerpartlemd  27942  ballotleme  28072  signsw0g  28150  signswmnd  28151  lgamgulmlem2  28209  lgamgulmlem3  28210  lgamgulmlem5  28212  lgambdd  28216  lgamcvglem  28219  derangenlem  28252  subfacp1lem3  28263  subfacp1lem5  28265  subfacp1lem6  28266  subfacp1  28267  erdszelem8  28279  kur14  28297  cnpcon  28312  rescon  28328  cvmscbv  28340  iscvm  28341  cvmsi  28347  cvmsval  28348  cvmlift3lem2  28402  snmlval  28413  ghomgrpilem1  28497  dfpo2  28758  dfon2lem9  28797  dfrdg2  28802  dfrdg3  28803  poseq  28907  soseq  28908  wrecseq123  28911  wfrlem1  28917  wfrlem15  28931  frrlem1  28961  sltval  28981  nocvxminlem  29024  nobndlem2  29027  nobndlem8  29033  nobndup  29034  nobnddown  29035  fin2so  29614  supaddc  29615  supadd  29616  heicant  29624  mblfinlem1  29626  mblfinlem2  29627  mblfinlem3  29628  ismblfin  29630  voliunnfl  29633  volsupnfl  29634  mbfresfi  29636  itg2addnc  29644  ftc1anc  29673  nn0prpwlem  29715  isfne  29738  isfne4  29739  isfne2  29741  isfne3  29742  isref  29749  islocfin  29766  neibastop3  29781  topmeet  29783  topjoin  29784  filnetlem4  29800  f1opr  29816  upixp  29821  indexdom  29826  filbcmb  29832  sdclem2  29836  fdc  29839  lmclim2  29852  caures  29854  istotbnd  29866  istotbnd3  29868  sstotbnd  29872  isbnd  29877  heibor  29918  bfp  29921  rrncmslem  29929  exidres  29941  exidresid  29942  idlval  30011  isidl  30012  0idl  30023  unichnidl  30029  pridl  30035  ismaxidl  30038  smprngopr  30050  igenval2  30064  prnc  30065  ispridlc  30068  scottexf  30178  scott0f  30179  isnacs  30238  isnacs2  30240  nacsfix  30246  mzpclval  30259  elmzpcl  30260  rencldnfilem  30356  infmrgelbi  30416  pellfundre  30419  pellfundlb  30422  wepwsolem  30591  fnwe2lem2  30601  aomclem8  30611  dfac11  30612  gicabl  30651  islnr3  30668  hbtlem2  30677  hbtlem5  30681  evth2f  30968  ubelsupr  30973  evthf  30980  fnchoice  30982  dstregt0  31040  upbdrech2  31085  ellimcabssub0  31159  limcdm0  31160  climf  31164  constlimc  31166  clim2f  31178  limsupre  31183  limcleqr  31186  addlimc  31190  0ellimcdiv  31191  clim2cf  31192  clim0cf  31196  cncfshift  31212  cncfperiod  31217  fperdvper  31248  dvdivbd  31253  dvbdfbdioo  31260  ioodvbdlimc1lem1  31261  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  stoweidlem5  31305  stoweidlem9  31309  stoweidlem15  31315  stoweidlem16  31316  stoweidlem27  31327  stoweidlem28  31328  stoweidlem31  31331  stoweidlem34  31334  stoweidlem37  31337  stoweidlem46  31346  stoweidlem48  31348  stoweidlem51  31351  stoweidlem52  31352  stoweidlem59  31359  wallispilem3  31367  stirlinglem13  31386  fourierdlem2  31409  fourierdlem3  31410  fourierdlem16  31423  fourierdlem20  31427  fourierdlem21  31428  fourierdlem22  31429  fourierdlem25  31432  fourierdlem39  31446  fourierdlem42  31449  fourierdlem45  31452  fourierdlem54  31461  fourierdlem64  31471  fourierdlem77  31484  fourierdlem83  31490  fourierdlem87  31494  fourierdlem103  31510  fourierdlem104  31511  cbvral2  31644  raaan2  31647  2reu4a  31661  dfdfat2  31683  ply1mulgsumlem1  32059  ply1mulgsumlem2  32060  linindslinci  32122  lindslinindsimp1  32131  lindslinindsimp2lem5  32136  lindslinindsimp2  32137  linds0  32139  lindsrng01  32142  snlindsntor  32145  mnd1  32161  grp1  32162  abl1  32163  rng1  32165  lmod1  32174  ldepsnlinc  32190  bnj1185  32931  bnj1385  32970  bnj66  32997  bnj106  33005  bnj155  33016  bnj852  33058  bnj893  33065  bnj1228  33146  bnj1234  33148  bnj1463  33190  riotasvd  33759  islfl  33857  eqlkr  33896  eqlkr3  33898  glbconN  34173  hlsuprexch  34177  ispsubsp  34541  ldilset  34905  isldil  34906  dilsetN  34949  isdilN  34950  trlset  34957  trlval  34958  cdleme27b  35164  cdleme29b  35171  cdleme31so  35175  cdleme31sn1  35177  cdleme31sn1c  35184  cdleme31fv  35186  cdleme40v  35265  istendo  35556  cdlemkid3N  35729  cdlemkid4  35730  cdlemkid5  35731  dihfval  36028  dihval  36029  islpolN  36280  hdmapffval  36626  hdmapfval  36627  hdmapval  36628  hdmapval2lem  36631  hgmapffval  36685  hgmapfval  36686  hgmapval  36687  hgmapvs  36691  taupilemrplb  36766  fiinfi  36778