Theorem ralbidv 2730

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 1673	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	ralbid 2728	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

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

This theorem is referenced by:  ralbii  2734  2ralbidv  2752  rexralbidv  2754  raleqbi1dv  2920  raleqbidv  2926  cbvral2v  2950  rspc2  3073  rspc3v  3077  reu6i  3145  reu7  3149  sbcralt  3262  raaan  3782  raaanv  3783  r19.12sn  3936  2ralunsn  4075  elintg  4131  elintrabg  4136  eliin  4171  disjprg  4283  disjxun  4285  reusv2lem2  4489  reusv3  4495  reusv6OLD  4498  poeq1  4639  somo  4670  frirr  4692  fr2nr  4693  frminex  4695  wereu2  4712  posn  4902  frsn  4904  ralxpf  4981  cnvpo  5370  fnmptfvd  5801  iinpreima  5828  dff4  5852  dff13f  5968  eusvobj2  6079  ofreq  6318  sorpssuni  6364  sorpssint  6365  fr3nr  6386  onssmin  6403  funcnvuni  6525  f1oweALT  6556  frxp  6677  smoeq  6803  recseq  6825  tfrlem12  6840  tz7.48lem  6888  elixp2  7259  undifixp  7291  xpf1o  7465  nneneq  7486  ac6sfi  7548  frfi  7549  fipreima  7609  indexfi  7611  marypha1lem  7675  marypha1  7676  supeq1  7687  supeq3  7691  supmo  7694  eqsup  7698  supub  7701  suplub  7702  supmaxlem  7706  supisoex  7713  oieq1  7718  ordtypecbv  7723  ordtypelem3  7726  ordtypelem6  7729  ordtypelem7  7730  ordtypelem9  7732  wemaplem1  7752  wemaplem2  7753  zfregcl  7801  oemapval  7883  oemapvali  7884  cantnf  7893  cantnfOLD  7915  wemapwe  7920  wemapweOLD  7921  rankval3b  8025  unbndrank  8041  rankunb  8049  rankuni2b  8052  tcrank  8083  scottex  8084  scottexs  8086  scott0s  8087  bnd2  8092  dfac8clem  8194  ac5num  8198  acni  8207  acni2  8208  alephval3  8272  dfac4  8284  dfac5lem5  8289  dfac5  8290  dfac2a  8291  dfac2  8292  dfacacn  8302  kmlem2  8312  kmlem13  8323  cflem  8407  cflecard  8414  cfeq0  8417  cfsuc  8418  cfflb  8420  cofsmo  8430  cfsmolem  8431  cfcoflem  8433  coftr  8434  alephsing  8437  fin23lem11  8478  isfin3ds  8490  fin23lem17  8499  fin23lem39  8511  isf33lem  8527  isf34lem6  8541  fin1a2lem13  8573  hsmexlem4  8590  hsmex  8593  axcc2lem  8597  axcc3  8599  dcomex  8608  axdc2lem  8609  axdc3lem2  8612  axdc3lem3  8613  axdc3  8615  axdc4lem  8616  axcclem  8618  zorn2lem2  8658  zorn2lem7  8663  zorn2g  8664  zornn0g  8666  ttukeylem7  8676  axdclem2  8681  brdom3  8687  brdom7disj  8690  brdom6disj  8691  alephval2  8728  inar1  8934  axgroth6  8987  pinq  9088  nqereu  9090  prlem934  9194  supexpr  9215  supsrlem  9270  axpre-sup  9328  dedekind  9525  dedekindle  9526  fimaxre2  10270  lbreu  10272  sup2  10278  infm3  10281  supmul1  10287  supmullem2  10289  supmul  10290  infmrcl  10301  nnsub  10352  uzwo  10909  uzwoOLD  10910  nnwof  10913  uzinfmi  10926  ublbneg  10931  lbzbi  10935  zsupss  10936  uzsupss  10939  uzwo3  10940  zmax  10942  rpnnen1lem1  10971  rpnnen1lem2  10972  rpnnen1lem3  10973  rpnnen1lem4  10974  rpnnen1lem5  10975  xrsupsslem  11261  xrinfmsslem  11262  xrsupss  11263  xrinfmss  11264  iccsupr  11374  supicc  11425  supiccub  11426  supicclub  11427  flval2  11654  flval3  11655  fsequb  11789  axdc4uzlem  11796  faclbnd4lem4  12064  bccl  12090  hashgt12el  12165  hashge2el2dif  12176  hashbc  12198  wrdind  12363  wrd2ind  12364  sqrlem3  12726  rexanre  12826  rexico  12833  cau4  12836  caubnd2  12837  caubnd  12838  clim  12964  rlim  12965  rlim2  12966  rlim2lt  12967  rlim3  12968  clim2  12974  clim2c  12975  clim0c  12977  rlim0  12978  rlim0lt  12979  ello12r  12987  ello1d  12993  lo1bdd2  12994  lo1bddrp  12995  elo12r  12998  rlimconst  13014  rlimresb  13035  rlimcld2  13048  climabs0  13055  rlimcn2  13060  reccn2  13066  cn1lem  13067  rlimo1  13086  o1rlimmul  13088  lo1add  13096  lo1mul  13097  isercoll  13137  caucvgrlem  13142  incexclem  13291  climcnds  13306  divrcnv  13307  ruclem12  13515  sqr2irr  13523  gcdcllem1  13687  gcdcllem2  13688  maxprmfct  13791  reumodprminv  13864  pc2dvds  13937  pcz  13939  prmpwdvds  13957  infpn2  13966  prmreclem1  13969  prmreclem2  13970  prmreclem3  13971  prmreclem5  13973  prmreclem6  13974  vdwlem6  14039  vdwlem8  14041  vdwlem13  14046  vdwnnlem1  14048  vdwnn  14051  ramz  14078  ramcl  14082  cshwrepswhash1  14121  prdsleval  14407  imasval  14441  imasaddfnlem  14458  imasvscafn  14467  mrisval  14560  isacs  14581  isacs2  14583  isacs1i  14587  mreacs  14588  acsfn  14589  acsfn2  14593  iscatd  14603  catidex  14604  catideu  14605  cidval  14607  catidd  14610  comfeq  14637  catpropd  14640  ismon  14664  isfunc  14766  isnat  14849  isprs  15092  drsdirfi  15100  ispos  15109  lubfval  15140  lubeldm  15143  lubval  15146  lubprop  15148  lublecllem  15150  glbfval  15153  glbeldm  15156  glbval  15159  glbprop  15161  joinval2lem  15170  joinlem  15173  meetval2lem  15184  meetlem  15187  isglbd  15279  lubl  15282  lubun  15285  clatleglb  15288  poslubmo  15308  posglbmo  15309  poslubd  15310  ipodrsima  15327  isdlat  15355  mgmidmo  15410  ismgmid  15427  ismgmid2  15430  ismndd  15436  mhmima  15482  mrcmndind  15485  gsumvallem1  15491  gsumvallem2  15492  gsumvalx  15493  gsumress  15498  gsumval2  15504  gsumwspan  15515  isgrpinv  15579  issubg4  15691  0subg  15697  cycsubgcl  15698  isnsg2  15702  nsgacs  15708  elnmz  15711  ghmrn  15751  ghmnsgima  15761  isga  15800  orbsta  15822  cntzfval  15829  elcntz  15831  resscntz  15840  oppgsubg  15869  symgextfo  15918  gsmsymgreqlem2  15927  gsmsymgreq  15928  pmtrdifel  15977  pmtrdifwrdellem3  15980  pmtrdifwrdel  15982  pmtrdifwrdel2  15983  psgnunilem2  15992  psgnunilem3  15993  odeq  16044  gexid  16071  gexlem2  16072  gexdvds  16074  isslw  16098  pgpssslw  16104  sylow2alem1  16107  sylow2alem2  16108  efgval  16205  efgrelexlemb  16238  efgcpbllemb  16243  gexex  16326  dmdprd  16468  dprd2da  16529  pgpfac1lem5  16568  isabv  16882  islss  16993  lssacs  17025  reslmhm  17110  islbs  17134  pj1lmhm  17158  lbsacsbs  17214  isrrg  17336  opsrval  17531  zringlpir  17881  zlpir  17886  psgndiflemA  18006  ocvfval  18066  elocv  18068  iunocv  18081  frlmlbs  18200  islindf  18216  islinds2  18217  islindf2  18218  lindfrn  18225  lsslindf  18234  islindf4  18242  mdetunilem1  18393  mdetunilem9  18401  basgen2  18569  bastop1  18573  isclo  18666  ordtbaslem  18767  iscn  18814  cnpval  18815  iscnp  18816  iscnp3  18823  lmbr  18837  lmbr2  18838  lmbrf  18839  cnprest  18868  cnprest2  18869  t0sep  18903  isreg  18911  t1sep2  18948  tgcmp  18979  1stcclb  19023  1stcfb  19024  2ndc1stc  19030  1stcrest  19032  2ndcdisj  19035  islly  19047  isnlly  19048  lly1stc  19075  elkgen  19084  kgencn  19104  elpt  19120  elptr  19121  ptcnplem  19169  tx1stc  19198  cnmpt21  19219  kqt0lem  19284  isr0  19285  regr1lem2  19288  r0sep  19296  nrmr0reg  19297  flffbas  19543  cnflf  19550  cnflf2  19551  lmflf  19553  txflf  19554  fclsopni  19563  fclsnei  19567  fclsrest  19572  fcfnei  19583  cnfcf  19590  alexsubb  19593  alexsubALTlem3  19596  divstgplem  19666  tsmsfbas  19673  tsmsgsum  19684  tsmsgsumOLD  19687  tsmsresOLD  19692  tsmsres  19693  tsmsf1o  19694  tsmsxplem1  19702  tsmsxp  19704  ustval  19752  isust  19753  ustincl  19757  ustdiag  19758  ustinvel  19759  ustexhalf  19760  ust0  19769  utopval  19782  ucnval  19827  isucn  19828  isucn2  19829  ucnima  19831  iscfilu  19838  ispsmet  19855  ismet  19873  isxmet  19874  imasdsf1olem  19923  imasf1oxmet  19925  imasf1omet  19926  metss  20058  met1stc  20071  prdsxmslem2  20079  metcnpi3  20096  txmetcnp  20097  metucnOLD  20138  metucn  20139  nlmvscn  20243  nrginvrcnlem  20246  nmoval  20269  nmolb  20271  nghmcn  20299  qtopbaslem  20312  icccmplem2  20375  icccmplem3  20376  reconnlem2  20379  metdscn  20407  cncfval  20439  elcncf2  20441  elcncf1di  20446  mulc1cncf  20456  cncfmet  20459  cnllycmp  20503  evth  20506  lebnumlem3  20510  lebnum  20511  xlebnum  20512  ishtpy  20519  isphtpy  20528  pi1xfr  20602  pi1coghm  20608  ipcn  20733  lmmbr2  20745  lmmbr3  20746  lmmbrf  20748  cfilfval  20750  iscfil  20751  fmcfil  20758  caufval  20761  iscau  20762  iscau2  20763  iscau3  20764  iscau4  20765  iscauf  20766  caucfil  20769  cfilresi  20781  causs  20784  lmclim  20788  cncmet  20808  cmetcusp1OLD  20838  cmetcusp1  20839  minveclem4c  20887  minveclem2  20888  minveclem3b  20890  minveclem4  20894  minveclem6  20896  minveclem7  20897  ivthlem2  20911  ivthlem3  20912  cniccbdd  20920  ovolunlem1  20955  ovoliunlem1  20960  ovoliun2  20964  ovolicc2lem3  20977  ismbl  20984  ioombl1lem4  21017  uniioombllem2  21038  uniioombllem6  21043  dyadmax  21053  dyadmbllem  21054  dyadmbl  21055  opnmbllem  21056  volcn  21061  ismbf1  21079  ismbf  21083  mbfeqalem  21095  mbfinf  21118  mbflimsup  21119  itg1climres  21167  mbfi1fseqlem6  21173  mbfi1flimlem  21175  itg2seq  21195  itg2monolem1  21203  itg2i1fseq  21208  itg2i1fseq2  21209  itg2cnlem1  21214  itg2cnlem2  21215  isibl  21218  dveflem  21426  ply1divex  21583  fta1g  21614  plyeq0lem  21653  dgrco  21717  plydivex  21738  fta1  21749  vieta1  21753  aannenlem1  21769  aannenlem2  21770  aalioulem2  21774  aalioulem3  21775  ulmval  21820  ulm2  21825  ulmi  21826  ulmres  21828  ulmshftlem  21829  ulmcaulem  21834  ulmcau  21835  ulmss  21837  ulmbdd  21838  ulmdvlem1  21840  ulmdvlem3  21842  mtestbdd  21845  iblulm  21847  abelthlem8  21879  pilem2  21892  pilem3  21893  divlogrlim  22055  cxpcn3  22161  dmarea  22326  rlimcnp  22334  cxplim  22340  cxploglim  22346  scvxcvx  22354  emcllem6  22369  ftalem1  22385  ftalem2  22386  ftalem3  22387  isppw2  22428  perfectlem2  22544  2sqlem6  22683  2sqlem10  22688  dchrisumlema  22712  dchrisumlem2  22714  dchrisumlem3  22715  dchrisum0  22744  pntpbnd  22812  pntibndlem3  22816  pntibnd  22817  pntleme  22832  pntlem3  22833  pntlemp  22834  pnt3  22836  axtg5seg  22901  brbtwn2  23102  colinearalg  23107  axsegconlem1  23114  axsegcon  23124  ax5seglem4  23129  ax5seglem5  23130  axlowdim  23158  axeuclidlem  23159  axcontlem1  23161  axcontlem2  23162  axcontlem4  23164  axcontlem5  23165  axcontlem8  23168  axcontlem12  23172  cusgra3v  23323  wlks  23376  wlkntrllem3  23411  constr3trllem2  23488  1conngra  23512  iseupa  23537  isgrpo  23634  isgrpo2  23635  isgrpoi  23636  grpoideu  23647  grpoidinv2  23656  isgrp2d  23673  isgrpda  23735  exidu1  23764  cmpidelt  23767  cnid  23789  mulid  23794  ghgrp  23806  isrngod  23817  rngoideu  23822  cnrngo  23841  vci  23877  isvclem  23906  isnvlem  23939  nvi  23943  nmcvcn  24041  lnoval  24103  islno  24104  isblo3i  24152  blo3i  24153  blocnilem  24155  blocni  24156  ajfval  24160  ubthlem1  24222  ubthlem2  24223  ubthlem3  24224  ubth  24225  minvecolem2  24227  minvecolem3  24228  minvecolem4c  24231  minvecolem4  24232  minvecolem5  24233  minvecolem6  24234  minvecolem7  24235  htthlem  24270  h2hcau  24332  h2hlm  24333  hilid  24514  hcau  24537  hlimi  24541  hlim2  24545  ocel  24635  adjsym  25188  ellnop  25213  ellnfn  25238  hhcno  25259  hhcnf  25260  0cnop  25334  0cnfn  25335  idcnop  25336  lnopeq  25364  elunop2  25368  lnophm  25374  lnconi  25388  lnopcnbd  25391  lnfncnbd  25412  imaelshi  25413  riesz3i  25417  riesz4i  25418  riesz4  25419  riesz1  25420  cnlnadjlem2  25423  cnlnadjlem5  25426  cnlnadjlem8  25429  cnlnadji  25431  nmopadjlei  25443  cnvbraval  25465  leopg  25477  leoppos  25481  mdbr  25649  dmdbr  25654  cdj3i  25796  rmoeq  25822  disjunsn  25887  funcnv5mpt  25939  fgreu  25941  xrge0infss  26004  resspos  26071  isomnd  26115  inftmrel  26148  isinftm  26149  archiabl  26166  rngurd  26207  isarchiofld  26236  rge0scvg  26331  qqhcn  26372  esumpcvgval  26479  sigaval  26505  issgon  26518  isrnmeas  26566  ismbfm  26619  isanmbfm  26623  mbfmcst  26626  sitgval  26670  oddpwdc  26689  eulerpartlemd  26701  ballotleme  26831  signsw0g  26909  signswmnd  26910  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem5  26971  lgambdd  26975  lgamcvglem  26978  derangenlem  27011  subfacp1lem3  27022  subfacp1lem5  27024  subfacp1lem6  27025  subfacp1  27026  erdszelem8  27038  kur14  27056  cnpcon  27071  rescon  27087  cvmscbv  27099  iscvm  27100  cvmsi  27106  cvmsval  27107  cvmlift3lem2  27161  snmlval  27172  ghomgrpilem1  27255  dfpo2  27516  dfon2lem9  27555  dfrdg2  27560  dfrdg3  27561  poseq  27665  soseq  27666  wrecseq123  27669  wfrlem1  27675  wfrlem15  27689  frrlem1  27719  sltval  27739  nocvxminlem  27782  nobndlem2  27785  nobndlem8  27791  nobndup  27792  nobnddown  27793  fin2so  28369  supaddc  28370  supadd  28371  heicant  28379  mblfinlem1  28381  mblfinlem2  28382  mblfinlem3  28383  ismblfin  28385  voliunnfl  28388  volsupnfl  28389  mbfresfi  28391  itg2addnc  28399  ftc1anc  28428  nn0prpwlem  28470  isfne  28493  isfne4  28494  isfne2  28496  isfne3  28497  isref  28504  islocfin  28521  neibastop3  28536  topmeet  28538  topjoin  28539  filnetlem4  28555  f1opr  28571  upixp  28576  indexdom  28581  filbcmb  28587  sdclem2  28591  fdc  28594  lmclim2  28607  caures  28609  istotbnd  28621  istotbnd3  28623  sstotbnd  28627  isbnd  28632  heibor  28673  bfp  28676  rrncmslem  28684  exidres  28696  exidresid  28697  idlval  28766  isidl  28767  0idl  28778  unichnidl  28784  pridl  28790  ismaxidl  28793  smprngopr  28805  igenval2  28819  prnc  28820  ispridlc  28823  scottexf  28933  scott0f  28934  isnacs  28993  isnacs2  28995  nacsfix  29001  mzpclval  29014  elmzpcl  29015  rencldnfilem  29112  infmrgelbi  29172  pellfundre  29175  pellfundlb  29178  wepwsolem  29347  fnwe2lem2  29357  aomclem8  29367  dfac11  29368  gicabl  29407  islnr3  29424  hbtlem2  29433  hbtlem5  29437  evth2f  29690  ubelsupr  29695  evthf  29702  fnchoice  29704  stoweidlem5  29753  stoweidlem9  29757  stoweidlem15  29763  stoweidlem16  29764  stoweidlem27  29775  stoweidlem28  29776  stoweidlem31  29779  stoweidlem34  29782  stoweidlem37  29785  stoweidlem46  29794  stoweidlem48  29796  stoweidlem51  29799  stoweidlem52  29800  stoweidlem59  29807  wallispilem3  29815  stirlinglem13  29834  cbvral2  29949  raaan2  29952  2reu4a  29966  dfdfat2  29990  wlkelwrd  30233  wlkcompim  30240  wwlk  30268  clwwlk  30382  rusgra0edg  30526  frgrawopreg1  30596  frgrawopreg2  30597  frgrareg  30663  frgraregord013  30664  ssnn0fi  30697  fsuppmapnn0fiubex  30749  mat0dimcrng  30789  dmatelnd  30798  dmatsubcl  30800  dmatmulcl  30802  scmatmulcl  30809  linindslinci  30871  lindslinindsimp1  30880  lindslinindsimp2lem5  30885  lindslinindsimp2  30886  linds0  30888  lindsrng01  30891  snlindsntor  30894  mnd1  30910  grp1  30911  abl1  30912  rng1  30914  lmod1  30923  ldepsnlinc  30939  bnj1185  31674  bnj1385  31713  bnj66  31740  bnj106  31748  bnj155  31759  bnj852  31801  bnj893  31808  bnj1228  31889  bnj1234  31891  bnj1463  31933  riotasvd  32447  islfl  32545  eqlkr  32584  eqlkr3  32586  glbconN  32861  hlsuprexch  32865  ispsubsp  33229  ldilset  33593  isldil  33594  dilsetN  33637  isdilN  33638  trlset  33645  trlval  33646  cdleme27b  33852  cdleme29b  33859  cdleme31so  33863  cdleme31sn1  33865  cdleme31sn1c  33872  cdleme31fv  33874  cdleme40v  33953  istendo  34244  cdlemkid3N  34417  cdlemkid4  34418  cdlemkid5  34419  dihfval  34716  dihval  34717  islpolN  34968  hdmapffval  35314  hdmapfval  35315  hdmapval  35316  hdmapval2lem  35319  hgmapffval  35373  hgmapfval  35374  hgmapval  35375  hgmapvs  35379  taupilemrplb  35454