Theorem ralbidv 2821

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 463	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	ralbidva 2818	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1826   A.wral 2732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712

This theorem depends on definitions:  df-bi 185  df-an 369  df-ral 2737

This theorem is referenced by:  2ralbidv  2826  ralbiiOLD  2896  rexralbidv  2901  raleqbi1dv  2987  raleqbidv  2993  cbvral2v  3017  rspc2  3143  rspc3v  3147  reu6i  3215  reu7  3219  sbcralt  3325  raaan  3853  raaanv  3854  2ralsng  3981  r19.12snOLD  4010  2ralunsn  4152  elintg  4207  elintrabg  4212  eliin  4249  disjprg  4363  disjxun  4365  reusv2lem2  4567  reusv3  4573  poeq1  4717  somo  4748  frirr  4770  fr2nr  4771  frminex  4773  wereu2  4790  posn  4982  frsn  4984  ralxpf  5062  cnvpo  5454  fnmptfvd  5892  iinpreima  5919  dff4  5947  dff13f  6068  eusvobj2  6189  ofreq  6442  sorpssuni  6488  sorpssint  6489  fr3nr  6514  onssmin  6531  funcnvuni  6652  f1oweALT  6683  frxp  6809  smoeq  6939  recseq  6961  tfrlem12  6976  tz7.48lem  7024  elixp2  7392  undifixp  7424  xpf1o  7598  nneneq  7619  ac6sfi  7679  frfi  7680  fipreima  7741  indexfi  7743  marypha1lem  7808  marypha1  7809  supeq1  7819  supeq3  7823  supmo  7826  eqsup  7830  supub  7833  suplub  7834  supmaxlemOLD  7839  supisoex  7847  oieq1  7852  ordtypecbv  7857  ordtypelem3  7860  ordtypelem6  7863  ordtypelem7  7864  ordtypelem9  7866  wemaplem1  7886  wemaplem2  7887  zfregcl  7935  oemapval  8015  oemapvali  8016  cantnf  8025  cantnfOLD  8047  wemapwe  8052  wemapweOLD  8053  rankval3b  8157  unbndrank  8173  rankunb  8181  rankuni2b  8184  tcrank  8215  scottex  8216  scottexs  8218  scott0s  8219  bnd2  8224  dfac8clem  8326  ac5num  8330  acni  8339  acni2  8340  alephval3  8404  dfac4  8416  dfac5lem5  8421  dfac5  8422  dfac2a  8423  dfac2  8424  dfacacn  8434  kmlem2  8444  kmlem13  8455  cflem  8539  cflecard  8546  cfeq0  8549  cfsuc  8550  cfflb  8552  cofsmo  8562  cfsmolem  8563  cfcoflem  8565  coftr  8566  alephsing  8569  fin23lem11  8610  isfin3ds  8622  fin23lem17  8631  fin23lem39  8643  isf33lem  8659  isf34lem6  8673  fin1a2lem13  8705  hsmexlem4  8722  hsmex  8725  axcc2lem  8729  axcc3  8731  dcomex  8740  axdc2lem  8741  axdc3lem2  8744  axdc3lem3  8745  axdc3  8747  axdc4lem  8748  axcclem  8750  zorn2lem2  8790  zorn2lem7  8795  zorn2g  8796  zornn0g  8798  ttukeylem7  8808  axdclem2  8813  brdom3  8819  brdom7disj  8822  brdom6disj  8823  alephval2  8860  inar1  9064  axgroth6  9117  pinq  9216  nqereu  9218  prlem934  9322  supexpr  9343  supsrlem  9399  axpre-sup  9457  dedekind  9655  dedekindle  9656  fimaxre2  10407  lbreu  10409  sup2  10415  infm3  10418  supmul1  10424  supmullem2  10426  supmul  10427  infmrcl  10438  nnsub  10491  uzwo  11064  nnwof  11067  uzinfmi  11080  ublbneg  11085  lbzbi  11089  zsupss  11090  uzsupss  11093  uzwo3  11096  zmax  11098  rpnnen1lem1  11127  rpnnen1lem2  11128  rpnnen1lem3  11129  rpnnen1lem4  11130  rpnnen1lem5  11131  xrsupsslem  11419  xrinfmsslem  11420  xrsupss  11421  xrinfmss  11422  iccsupr  11538  supicc  11589  supiccub  11590  supicclub  11591  flval2  11849  flval3  11850  fsequb  11988  axdc4uzlem  11995  ssnn0fi  11997  fsuppmapnn0fiubex  12001  faclbnd4lem4  12276  bccl  12302  hashgt12el  12385  hashbc  12406  hashge2el2dif  12425  wrdind  12613  wrd2ind  12614  sqrlem3  13080  rexanre  13181  rexico  13188  cau4  13191  caubnd2  13192  caubnd  13193  clim  13319  rlim  13320  rlim2  13321  rlim2lt  13322  rlim3  13323  clim2  13329  clim2c  13330  clim0c  13332  rlim0  13333  rlim0lt  13334  ello12r  13342  ello1d  13348  lo1bdd2  13349  lo1bddrp  13350  elo12r  13353  rlimconst  13369  rlimresb  13390  rlimcld2  13403  climabs0  13410  rlimcn2  13415  reccn2  13421  cn1lem  13422  rlimo1  13441  o1rlimmul  13443  lo1add  13451  lo1mul  13452  isercoll  13492  caucvgrlem  13497  incexclem  13650  climcnds  13665  divrcnv  13666  ruclem12  13976  sqrt2irr  13984  gcdcllem1  14151  gcdcllem2  14152  maxprmfct  14256  reumodprminv  14331  pc2dvds  14404  pcz  14406  prmpwdvds  14424  infpn2  14433  prmreclem1  14436  prmreclem2  14437  prmreclem3  14438  prmreclem5  14440  prmreclem6  14441  vdwlem6  14506  vdwlem8  14508  vdwlem13  14513  vdwnnlem1  14515  vdwnn  14518  ramz  14545  ramcl  14549  cshwrepswhash1  14589  prdsleval  14884  imasval  14918  imasaddfnlem  14935  imasvscafn  14944  mrisval  15037  isacs  15058  isacs2  15060  isacs1i  15064  mreacs  15065  acsfn  15066  acsfn2  15070  iscatd  15080  catidex  15081  catideu  15082  cidval  15084  catidd  15087  comfeq  15112  catpropd  15115  ismon  15139  isfunc  15270  isnat  15353  isinito  15396  istermo  15397  isprs  15676  drsdirfi  15684  ispos  15693  lubfval  15725  lubeldm  15728  lubval  15731  lubprop  15733  lublecllem  15735  glbfval  15738  glbeldm  15741  glbval  15744  glbprop  15746  joinval2lem  15755  joinlem  15758  meetval2lem  15769  meetlem  15772  isglbd  15864  lubl  15867  lubun  15870  clatleglb  15873  poslubmo  15893  posglbmo  15894  poslubd  15895  ipodrsima  15912  isdlat  15940  mgm1  16001  mgmidmo  16003  ismgmid  16008  ismgmid2  16011  mgmidsssn0  16013  gsumvalx  16014  gsumress  16020  gsumval2  16024  sgrp1  16035  mndclOLD  16048  mndassOLD  16049  ismndd  16060  mnd1  16078  mnd1OLD  16079  mhmima  16111  mrcmndind  16114  gsumvallem2  16120  gsumwspan  16131  sgrp2rid2  16161  sgrp2rid2ex  16162  sgrp2nmndlem4  16163  isgrpinv  16217  mhmmnd  16309  issubg4  16337  0subg  16343  cycsubgcl  16344  isnsg2  16348  nsgacs  16354  elnmz  16357  ghmrn  16397  ghmnsgima  16407  isga  16446  orbsta  16468  cntzfval  16475  elcntz  16477  resscntz  16486  oppgsubg  16515  symgextfo  16564  gsmsymgreqlem2  16573  gsmsymgreq  16574  pmtrdifel  16622  pmtrdifwrdellem3  16625  pmtrdifwrdel2  16628  psgnunilem2  16637  psgnunilem3  16638  odeq  16691  gexid  16718  gexlem2  16719  gexdvds  16721  isslw  16745  pgpssslw  16751  sylow2alem1  16754  sylow2alem2  16755  efgval  16852  efgrelexlemb  16885  efgcpbllemb  16890  gexex  16976  abl1  16989  dmdprd  17142  dprd2da  17204  pgpfac1lem5  17243  ring1  17361  isabv  17581  islss  17694  lssacs  17726  reslmhm  17811  islbs  17835  pj1lmhm  17859  lbsacsbs  17915  isrrg  18049  opsrval  18252  ply1coe  18450  cply1coe0bi  18455  zringlpir  18618  psgndiflemA  18728  ocvfval  18788  elocv  18790  iunocv  18803  frlmlbs  18917  islindf  18932  islinds2  18933  islindf2  18934  lindfrn  18941  lsslindf  18950  islindf4  18958  mat0dimcrng  19057  mdetunilem1  19199  mdetunilem9  19207  cpmat  19295  cpmatel  19297  1elcpmat  19301  m2cpminvid2lem  19340  chfacffsupp  19442  chfacfscmulfsupp  19445  chfacfpmmulfsupp  19449  basgen2  19576  bastop1  19580  isclo  19674  ordtbaslem  19775  iscn  19822  cnpval  19823  iscnp  19824  iscnp3  19831  lmbr  19845  lmbr2  19846  lmbrf  19847  cnprest  19876  cnprest2  19877  t0sep  19911  isreg  19919  t1sep2  19956  tgcmp  19987  1stcclb  20030  1stcfb  20031  2ndc1stc  20037  1stcrest  20039  2ndcdisj  20042  islly  20054  isnlly  20055  lly1stc  20082  isref  20095  islocfin  20103  elkgen  20122  kgencn  20142  elpt  20158  elptr  20159  ptcnplem  20207  tx1stc  20236  cnmpt21  20257  kqt0lem  20322  isr0  20323  regr1lem2  20326  r0sep  20334  nrmr0reg  20335  flffbas  20581  cnflf  20588  cnflf2  20589  lmflf  20591  txflf  20592  fclsopni  20601  fclsnei  20605  fclsrest  20610  fcfnei  20621  cnfcf  20628  alexsubb  20631  alexsubALTlem3  20634  qustgplem  20704  tsmsfbas  20711  tsmsgsum  20722  tsmsgsumOLD  20725  tsmsresOLD  20730  tsmsres  20731  tsmsf1o  20732  tsmsxplem1  20740  tsmsxp  20742  ustval  20790  isust  20791  ustincl  20795  ustdiag  20796  ustinvel  20797  ustexhalf  20798  ust0  20807  utopval  20820  ucnval  20865  isucn  20866  isucn2  20867  ucnima  20869  iscfilu  20876  ispsmet  20893  ismet  20911  isxmet  20912  imasdsf1olem  20961  imasf1oxmet  20963  imasf1omet  20964  metss  21096  met1stc  21109  prdsxmslem2  21117  metcnpi3  21134  txmetcnp  21135  metucnOLD  21176  metucn  21177  nlmvscn  21281  nrginvrcnlem  21284  nmoval  21307  nmolb  21309  nghmcn  21337  qtopbaslem  21350  icccmplem2  21413  icccmplem3  21414  reconnlem2  21417  metdscn  21445  cncfval  21477  elcncf2  21479  elcncf1di  21484  mulc1cncf  21494  cncfmet  21497  cnllycmp  21541  evth  21544  lebnumlem3  21548  lebnum  21549  xlebnum  21550  ishtpy  21557  isphtpy  21566  pi1xfr  21640  pi1coghm  21646  ipcn  21771  lmmbr2  21783  lmmbr3  21784  lmmbrf  21786  cfilfval  21788  iscfil  21789  fmcfil  21796  caufval  21799  iscau  21800  iscau2  21801  iscau3  21802  iscau4  21803  iscauf  21804  caucfil  21807  cfilresi  21819  causs  21822  lmclim  21826  cncmet  21846  cmetcusp1OLD  21876  cmetcusp1  21877  minveclem4c  21925  minveclem2  21926  minveclem3b  21928  minveclem4  21932  minveclem6  21934  minveclem7  21935  ivthlem2  21949  ivthlem3  21950  cniccbdd  21958  ovolunlem1  21993  ovoliunlem1  21998  ovoliun2  22002  ovolicc2lem3  22015  ismbl  22022  ioombl1lem4  22056  uniioombllem2  22077  uniioombllem6  22082  dyadmax  22092  dyadmbllem  22093  dyadmbl  22094  opnmbllem  22095  volcn  22100  ismbf1  22118  ismbf  22122  mbfeqalem  22134  mbfinf  22157  mbflimsup  22158  itg1climres  22206  mbfi1fseqlem6  22212  mbfi1flimlem  22214  itg2seq  22234  itg2monolem1  22242  itg2i1fseq  22247  itg2i1fseq2  22248  itg2cnlem1  22253  itg2cnlem2  22254  isibl  22257  dveflem  22465  ply1divex  22622  fta1g  22653  plyeq0lem  22692  dgrco  22757  plydivex  22778  fta1  22789  vieta1  22793  aannenlem1  22809  aannenlem2  22810  aalioulem2  22814  aalioulem3  22815  ulmval  22860  ulm2  22865  ulmi  22866  ulmres  22868  ulmshftlem  22869  ulmcaulem  22874  ulmcau  22875  ulmss  22877  ulmbdd  22878  ulmdvlem1  22880  ulmdvlem3  22882  mtestbdd  22885  iblulm  22887  abelthlem8  22919  pilem2  22932  pilem3  22933  divlogrlim  23103  cxpcn3  23209  dmarea  23404  rlimcnp  23412  cxplim  23418  cxploglim  23424  scvxcvx  23432  emcllem6  23447  ftalem1  23463  ftalem2  23464  ftalem3  23465  isppw2  23506  perfectlem2  23622  2sqlem6  23761  2sqlem10  23766  dchrisumlema  23790  dchrisumlem2  23792  dchrisumlem3  23793  dchrisum0  23822  pntpbnd  23890  pntibndlem3  23894  pntibnd  23895  pntleme  23910  pntlem3  23911  pntlemp  23912  pnt3  23914  istrkgld  23974  axtg5seg  23979  perpln1  24207  perpln2  24208  isperp  24209  brbtwn2  24329  colinearalg  24334  axsegconlem1  24341  axsegcon  24351  ax5seglem4  24356  ax5seglem5  24357  axlowdim  24385  axeuclidlem  24386  axcontlem1  24388  axcontlem2  24389  axcontlem4  24391  axcontlem5  24392  axcontlem8  24395  axcontlem12  24399  cusgra3v  24585  wlks  24640  wlkcompim  24647  wlkelwrd  24651  wlkntrllem3  24684  constr3trllem2  24772  1conngra  24796  wwlk  24802  clwwlk  24887  isrgrac  25055  rusgra0edg  25076  iseupa  25086  frgrawopreg1  25171  frgrawopreg2  25172  frgrareg  25238  frgraregord013  25239  isgrpo  25315  isgrpo2  25316  isgrpoi  25317  grpoideu  25328  grpoidinv2  25337  isgrp2d  25354  isgrpda  25416  exidu1  25445  cmpidelt  25448  cnid  25470  mulid  25475  ghgrpOLD  25487  isrngod  25498  rngoideu  25503  cnrngo  25522  vci  25558  isvclem  25587  isnvlem  25620  nvi  25624  nmcvcn  25722  lnoval  25784  islno  25785  isblo3i  25833  blo3i  25834  blocnilem  25836  blocni  25837  ajfval  25841  ubthlem1  25903  ubthlem2  25904  ubthlem3  25905  ubth  25906  minvecolem2  25908  minvecolem3  25909  minvecolem4c  25912  minvecolem4  25913  minvecolem5  25914  minvecolem6  25915  minvecolem7  25916  htthlem  25951  h2hcau  26013  h2hlm  26014  hilid  26195  hcau  26218  hlimi  26222  hlim2  26226  ocel  26316  adjsym  26868  ellnop  26893  ellnfn  26918  hhcno  26939  hhcnf  26940  0cnop  27014  0cnfn  27015  idcnop  27016  lnopeq  27044  elunop2  27048  lnophm  27054  lnconi  27068  lnopcnbd  27071  lnfncnbd  27092  imaelshi  27093  riesz3i  27097  riesz4i  27098  riesz4  27099  riesz1  27100  cnlnadjlem2  27103  cnlnadjlem5  27106  cnlnadjlem8  27109  cnlnadji  27111  nmopadjlei  27123  cnvbraval  27145  leopg  27157  leoppos  27161  mdbr  27329  dmdbr  27334  cdj3i  27476  rmoeq  27503  disjunsn  27583  funcnv5mpt  27657  fgreu  27659  fcnvgreu  27660  xrge0infss  27730  resspos  27800  isomnd  27844  inftmrel  27877  isinftm  27878  archiabl  27895  rngurd  27932  isarchiofld  27961  crefeq  28002  rge0scvg  28085  qqhcn  28125  esumpcvgval  28226  esum2d  28241  sigaval  28259  issgon  28272  isrnmeas  28327  ismbfm  28379  isanmbfm  28383  mbfmcst  28386  elcarsg  28432  sitgval  28457  oddpwdc  28476  eulerpartlemd  28488  ballotleme  28618  signsw0g  28696  signswmnd  28697  lgamgulmlem2  28761  lgamgulmlem3  28762  lgamgulmlem5  28764  lgambdd  28768  lgamcvglem  28771  derangenlem  28804  subfacp1lem3  28815  subfacp1lem5  28817  subfacp1lem6  28818  subfacp1  28819  erdszelem8  28831  kur14  28849  cnpcon  28864  rescon  28880  cvmscbv  28892  iscvm  28893  cvmsi  28899  cvmsval  28900  cvmlift3lem2  28954  snmlval  28965  mclsssvlem  29111  mclsval  29112  mclsax  29118  mclsind  29119  ghomgrpilem1  29214  dfpo2  29350  dfon2lem9  29388  dfrdg2  29393  dfrdg3  29394  poseq  29498  soseq  29499  wrecseq123  29502  wfrlem1  29508  wfrlem15  29522  frrlem1  29552  sltval  29572  nocvxminlem  29615  nobndlem2  29618  nobndlem8  29624  nobndup  29625  nobnddown  29626  fin2so  30205  supaddc  30206  supadd  30207  heicant  30214  mblfinlem1  30216  mblfinlem2  30217  mblfinlem3  30218  ismblfin  30220  voliunnfl  30223  volsupnfl  30224  mbfresfi  30226  itg2addnc  30235  ftc1anc  30264  nn0prpwlem  30306  isfne  30323  isfne4  30324  isfne2  30326  isfne3  30327  neibastop3  30346  topmeet  30348  topjoin  30349  filnetlem4  30365  f1opr  30381  upixp  30386  indexdom  30391  filbcmb  30397  sdclem2  30401  fdc  30404  lmclim2  30417  caures  30419  istotbnd  30431  istotbnd3  30433  sstotbnd  30437  isbnd  30442  heibor  30483  bfp  30486  rrncmslem  30494  exidres  30506  exidresid  30507  idlval  30576  isidl  30577  0idl  30588  unichnidl  30594  pridl  30600  ismaxidl  30603  smprngopr  30615  igenval2  30629  prnc  30630  ispridlc  30633  scottexf  30742  scott0f  30743  isnacs  30802  isnacs2  30804  nacsfix  30810  mzpclval  30823  elmzpcl  30824  rencldnfilem  30919  infmrgelbi  30979  pellfundre  30982  pellfundlb  30985  wepwsolem  31153  fnwe2lem2  31163  aomclem8  31173  dfac11  31174  gicabl  31215  islnr3  31232  hbtlem2  31241  hbtlem5  31245  evth2f  31557  ubelsupr  31562  evthf  31569  fnchoice  31571  dstregt0  31630  upbdrech2  31674  mccl  31772  mullimc  31788  ellimcabssub0  31789  limcdm0  31790  climf  31794  mullimcf  31795  constlimc  31796  idlimc  31798  clim2f  31808  limsupre  31813  limcleqr  31816  addlimc  31820  0ellimcdiv  31821  clim2cf  31822  clim0cf  31826  cncfshift  31842  cncfperiod  31847  fperdvper  31881  dvdivbd  31886  dvbdfbdioo  31893  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  dvnprodlem3  31911  stoweidlem5  31953  stoweidlem9  31957  stoweidlem15  31963  stoweidlem16  31964  stoweidlem27  31975  stoweidlem28  31976  stoweidlem31  31979  stoweidlem34  31982  stoweidlem37  31985  stoweidlem46  31994  stoweidlem48  31996  stoweidlem51  31999  stoweidlem52  32000  stoweidlem59  32007  wallispilem3  32015  stirlinglem13  32034  fourierdlem2  32057  fourierdlem3  32058  fourierdlem16  32071  fourierdlem20  32075  fourierdlem21  32076  fourierdlem22  32077  fourierdlem25  32080  fourierdlem39  32094  fourierdlem42  32097  fourierdlem54  32109  fourierdlem64  32119  fourierdlem77  32132  fourierdlem83  32138  fourierdlem87  32142  fourierdlem103  32158  fourierdlem104  32159  cbvral2  32343  raaan2  32346  2reu4a  32360  dfdfat2  32382  perfectALTVlem2  32544  mgmhmima  32808  rnghmval  32897  lidlmsgrp  32932  lidlrng  32933  zlidlring  32934  uzlidlring  32935  2zrngamnd  32947  ply1mulgsumlem1  33186  ply1mulgsumlem2  33187  linindslinci  33249  lindslinindsimp1  33258  lindslinindsimp2lem5  33263  lindslinindsimp2  33264  linds0  33266  lindsrng01  33269  snlindsntor  33272  lmod1  33293  ldepsnlinc  33309  bigoval  33370  elbigo2r  33374  nn0sumshdiglem2  33443  bnj1185  34199  bnj1385  34238  bnj66  34265  bnj106  34273  bnj155  34284  bnj852  34326  bnj893  34333  bnj1228  34414  bnj1234  34416  bnj1463  34458  riotasvd  35100  islfl  35198  eqlkr  35237  eqlkr3  35239  glbconN  35514  hlsuprexch  35518  ispsubsp  35882  ldilset  36246  isldil  36247  dilsetN  36291  isdilN  36292  trlset  36299  trlval  36300  cdleme27b  36507  cdleme29b  36514  cdleme31so  36518  cdleme31sn1  36520  cdleme31sn1c  36527  cdleme31fv  36529  cdleme40v  36608  istendo  36899  cdlemkid3N  37072  cdlemkid4  37073  cdlemkid5  37074  dihfval  37371  dihval  37372  islpolN  37623  hdmapffval  37969  hdmapfval  37970  hdmapval  37971  hdmapval2lem  37974  hgmapffval  38028  hgmapfval  38029  hgmapval  38030  hgmapvs  38034  taupilemrplb  38108  fiinfi  38187  imo72b2lem0  38511  imo72b2lem2  38513  imo72b2lem1  38517  imo72b2  38522