Theorem ralbidv 2686

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

Syntax hints:   -> wi 4   <-> wb 177   A.wral 2666

This theorem is referenced by:  ralbii  2690  2ralbidv  2708  rexralbidv  2710  raleqbi1dv  2872  raleqbidv  2876  cbvral2v  2900  rspc2  3017  rspc3v  3021  reu6i  3085  reu7  3089  sbcralt  3193  sbcralg  3195  raaan  3695  raaanv  3696  r19.12sn  3832  2ralunsn  3964  elintg  4018  elintrabg  4023  eliin  4058  disjprg  4168  disjxun  4170  poeq1  4466  somo  4497  frirr  4519  fr2nr  4520  frminex  4522  wereu2  4539  reusv2lem2  4684  reusv3  4690  reusv6OLD  4693  fr3nr  4719  onssmin  4736  posn  4905  frsn  4907  ralxpf  4978  cnvpo  5369  funcnvuni  5477  iinpreima  5819  dff4  5842  dff13f  5965  f1oweALT  6033  ofreq  6267  frxp  6415  sorpssuni  6490  sorpssint  6491  eusvobj2  6541  riotasvd  6551  smoeq  6571  recseq  6593  tfrlem3  6597  tfrlem3a  6598  tfrlem12  6609  tz7.48lem  6657  elixp2  7025  undifixp  7057  xpf1o  7228  nneneq  7249  ac6sfi  7310  frfi  7311  fipreima  7370  indexfi  7372  marypha1lem  7396  marypha1  7397  supeq1  7408  supmo  7413  eqsup  7417  supub  7420  suplub  7421  supmaxlem  7425  supisoex  7432  oieq1  7437  ordtypecbv  7442  ordtypelem3  7445  ordtypelem6  7448  ordtypelem7  7449  ordtypelem9  7451  wemaplem1  7471  wemaplem2  7472  zfregcl  7518  oemapval  7595  oemapvali  7596  cantnf  7605  wemapwe  7610  rankval3b  7708  unbndrank  7724  rankunb  7732  rankuni2b  7735  tcrank  7764  scottex  7765  scottexs  7767  scott0s  7768  bnd2  7773  dfac8clem  7869  ac5num  7873  acni  7882  acni2  7883  alephval3  7947  dfac4  7959  dfac5lem5  7964  dfac5  7965  dfac2a  7966  dfac2  7967  dfacacn  7977  kmlem2  7987  kmlem13  7998  cflem  8082  cflecard  8089  cfeq0  8092  cfsuc  8093  cfflb  8095  cofsmo  8105  cfsmolem  8106  cfcoflem  8108  coftr  8109  alephsing  8112  fin23lem11  8153  isfin3ds  8165  fin23lem17  8174  fin23lem39  8186  isf33lem  8202  isf34lem6  8216  fin1a2lem13  8248  hsmexlem4  8265  hsmex  8268  axcc2lem  8272  axcc3  8274  dcomex  8283  axdc2lem  8284  axdc3lem2  8287  axdc3lem3  8288  axdc3  8290  axdc4lem  8291  axcclem  8293  zorn2lem2  8333  zorn2lem7  8338  zorn2g  8339  zornn0g  8341  ttukeylem7  8351  axdclem2  8356  brdom3  8362  brdom7disj  8365  brdom6disj  8366  alephval2  8403  inar1  8606  axgroth6  8659  pinq  8760  nqereu  8762  prlem934  8866  supexpr  8887  supsrlem  8942  axpre-sup  9000  fimaxre2  9912  lbreu  9914  sup2  9920  infm3  9923  supmul1  9929  supmullem2  9931  supmul  9932  infmrcl  9943  nnsub  9994  uzwo  10495  uzwoOLD  10496  nnwof  10499  uzinfmi  10511  ublbneg  10516  lbzbi  10520  zsupss  10521  uzsupss  10524  uzwo3  10525  zmax  10527  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem4  10559  rpnnen1lem5  10560  xrsupsslem  10841  xrinfmsslem  10842  xrsupss  10843  xrinfmss  10844  iccsupr  10953  flval2  11176  flval3  11177  fsequb  11269  axdc4uzlem  11276  faclbnd4lem4  11542  bccl  11568  hashgt12el  11637  hashbc  11657  wrdind  11746  sqrlem3  12005  rexanre  12105  rexico  12112  cau4  12115  caubnd2  12116  caubnd  12117  clim  12243  rlim  12244  rlim2  12245  rlim2lt  12246  rlim3  12247  clim2  12253  clim2c  12254  clim0c  12256  rlim0  12257  rlim0lt  12258  ello12r  12266  ello1d  12272  lo1bdd2  12273  lo1bddrp  12274  elo12r  12277  rlimconst  12293  rlimresb  12314  rlimcld2  12327  climabs0  12334  rlimcn2  12339  reccn2  12345  cn1lem  12346  rlimo1  12365  o1rlimmul  12367  lo1add  12375  lo1mul  12376  isercoll  12416  caucvgrlem  12421  incexclem  12571  climcnds  12586  divrcnv  12587  ruclem12  12795  sqr2irr  12803  gcdcllem1  12966  gcdcllem2  12967  maxprmfct  13068  pc2dvds  13207  pcz  13209  prmpwdvds  13227  infpn2  13236  prmreclem1  13239  prmreclem2  13240  prmreclem3  13241  prmreclem5  13243  prmreclem6  13244  vdwlem6  13309  vdwlem8  13311  vdwlem13  13316  vdwnnlem1  13318  vdwnn  13321  ramz  13348  ramcl  13352  prdsleval  13654  imasval  13692  imasaddfnlem  13708  imasvscafn  13717  mrisval  13810  isacs  13831  isacs2  13833  isacs1i  13837  mreacs  13838  acsfn  13839  acsfn2  13843  iscatd  13853  catidex  13854  catideu  13855  cidval  13857  catidd  13860  comfeq  13887  catpropd  13890  ismon  13914  isfunc  14016  isnat  14099  isprs  14342  drsdirfi  14350  ispos  14359  lubfval  14390  lubval  14391  lubprop  14392  lubid  14394  glbfval  14395  glbval  14396  glbprop  14397  joinval2  14401  joinlem  14402  meetval2  14408  meetlem  14409  isglbd  14499  lubl  14502  lubun  14505  clatleglb  14508  poslubmo  14528  poslubd  14529  ipodrsima  14546  isdlat  14574  spwval2  14611  spwmo  14613  spwpr2  14615  spwpr4  14618  mgmidmo  14648  ismgmid  14665  ismgmid2  14668  ismndd  14674  mhmima  14718  gsumvallem1  14726  gsumvallem2  14727  gsumvalx  14729  gsumress  14732  gsumval2  14738  gsumwspan  14746  isgrpinv  14810  issubg4  14916  0subg  14920  cycsubgcl  14921  isnsg2  14925  nsgacs  14931  elnmz  14934  ghmrn  14974  ghmnsgima  14984  isga  15023  orbsta  15045  cntzfval  15074  elcntz  15076  resscntz  15085  oppgsubg  15114  odeq  15143  gexid  15170  gexlem2  15171  gexdvds  15173  isslw  15197  pgpssslw  15203  sylow2alem1  15206  sylow2alem2  15207  efgval  15304  efgrelexlemb  15337  efgcpbllemb  15342  gexex  15423  dmdprd  15514  dprd2da  15555  pgpfac1lem5  15592  isabv  15862  islss  15966  lssacs  15998  reslmhm  16083  islbs  16103  pj1lmhm  16127  lbsacsbs  16183  isrrg  16303  opsrval  16490  zlpir  16726  ocvfval  16848  elocv  16850  iunocv  16863  basgen2  17009  bastop1  17013  isclo  17106  ordtbaslem  17206  iscn  17253  cnpval  17254  iscnp  17255  iscnp3  17262  lmbr  17276  lmbr2  17277  lmbrf  17278  cnprest  17307  cnprest2  17308  t0sep  17342  isreg  17350  t1sep2  17387  tgcmp  17418  1stcclb  17460  1stcfb  17461  2ndc1stc  17467  1stcrest  17469  2ndcdisj  17472  islly  17484  isnlly  17485  lly1stc  17512  elkgen  17521  kgencn  17541  elpt  17557  elptr  17558  ptcnplem  17606  tx1stc  17635  cnmpt21  17656  kqt0lem  17721  isr0  17722  regr1lem2  17725  r0sep  17733  nrmr0reg  17734  flffbas  17980  cnflf  17987  cnflf2  17988  lmflf  17990  txflf  17991  fclsopni  18000  fclsnei  18004  fclsrest  18009  fcfnei  18020  cnfcf  18027  alexsubb  18030  alexsubALTlem3  18033  divstgplem  18103  tsmsfbas  18110  tsmsgsum  18121  tsmsres  18126  tsmsf1o  18127  tsmsxplem1  18135  tsmsxp  18137  ustval  18185  isust  18186  ustincl  18190  ustdiag  18191  ustinvel  18192  ustexhalf  18193  ust0  18202  utopval  18215  ucnval  18260  isucn  18261  isucn2  18262  ucnima  18264  iscfilu  18271  ispsmet  18288  ismet  18306  isxmet  18307  imasdsf1olem  18356  imasf1oxmet  18358  imasf1omet  18359  metss  18491  met1stc  18504  prdsxmslem2  18512  metcnpi3  18529  txmetcnp  18530  metucnOLD  18571  metucn  18572  nlmvscn  18676  nrginvrcnlem  18679  nmoval  18702  nmolb  18704  nghmcn  18732  qtopbaslem  18745  icccmplem2  18807  icccmplem3  18808  reconnlem2  18811  metdscn  18839  cncfval  18871  elcncf2  18873  elcncf1di  18878  mulc1cncf  18888  cncfmet  18891  cnllycmp  18934  evth  18937  lebnumlem3  18941  lebnum  18942  xlebnum  18943  ishtpy  18950  isphtpy  18959  pi1xfr  19033  pi1coghm  19039  ipcn  19153  lmmbr2  19165  lmmbr3  19166  lmmbrf  19168  cfilfval  19170  iscfil  19171  fmcfil  19178  caufval  19181  iscau  19182  iscau2  19183  iscau3  19184  iscau4  19185  iscauf  19186  caucfil  19189  cfilresi  19201  causs  19204  lmclim  19208  cncmet  19228  cmetcusp1OLD  19258  cmetcusp1  19259  minveclem4c  19279  minveclem2  19280  minveclem3b  19282  minveclem4  19286  minveclem6  19288  minveclem7  19289  ivthlem2  19302  ivthlem3  19303  cniccbdd  19311  ovolunlem1  19346  ovoliunlem1  19351  ovoliun2  19355  ovolicc2lem3  19368  ismbl  19375  ioombl1lem4  19408  uniioombllem2  19428  uniioombllem6  19433  dyadmax  19443  dyadmbllem  19444  dyadmbl  19445  opnmbllem  19446  volcn  19451  ismbf1  19471  ismbf  19475  mbfeqalem  19487  mbfinf  19510  mbflimsup  19511  itg1climres  19559  mbfi1fseqlem6  19565  mbfi1flimlem  19567  itg2seq  19587  itg2monolem1  19595  itg2i1fseq  19600  itg2i1fseq2  19601  itg2cnlem1  19606  itg2cnlem2  19607  isibl  19610  dveflem  19816  ply1divex  20012  fta1g  20043  plyeq0lem  20082  dgrco  20146  plydivex  20167  fta1  20178  vieta1  20182  aannenlem1  20198  aannenlem2  20199  aalioulem2  20203  aalioulem3  20204  ulmval  20249  ulm2  20254  ulmi  20255  ulmres  20257  ulmshftlem  20258  ulmcaulem  20263  ulmcau  20264  ulmss  20266  ulmbdd  20267  ulmdvlem1  20269  ulmdvlem3  20271  mtestbdd  20274  iblulm  20276  abelthlem8  20308  pilem2  20321  pilem3  20322  divlogrlim  20479  cxpcn3  20585  dmarea  20749  rlimcnp  20757  cxplim  20763  cxploglim  20769  scvxcvx  20777  emcllem6  20792  ftalem1  20808  ftalem2  20809  ftalem3  20810  isppw2  20851  perfectlem2  20967  2sqlem6  21106  2sqlem10  21111  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  dchrisum0  21167  pntpbnd  21235  pntibndlem3  21239  pntibnd  21240  pntleme  21255  pntlem3  21256  pntlemp  21257  pnt3  21259  cusgra3v  21426  wlks  21479  wlkntrllem3  21514  constr3trllem2  21591  1conngra  21615  iseupa  21640  isgrpo  21737  isgrpo2  21738  isgrpoi  21739  grpoideu  21750  grpoidinv2  21759  isgrp2d  21776  isgrpda  21838  exidu1  21867  cmpidelt  21870  cnid  21892  mulid  21897  ghgrp  21909  isrngod  21920  rngoideu  21925  cnrngo  21944  vci  21980  isvclem  22009  isnvlem  22042  nvi  22046  nmcvcn  22144  lnoval  22206  islno  22207  isblo3i  22255  blo3i  22256  blocnilem  22258  blocni  22259  ajfval  22263  ubthlem1  22325  ubthlem2  22326  ubthlem3  22327  ubth  22328  minvecolem2  22330  minvecolem3  22331  minvecolem4c  22334  minvecolem4  22335  minvecolem5  22336  minvecolem6  22337  minvecolem7  22338  htthlem  22373  h2hcau  22435  h2hlm  22436  hilid  22616  hcau  22639  hlimi  22643  hlim2  22647  ocel  22736  adjsym  23289  ellnop  23314  ellnfn  23339  hhcno  23360  hhcnf  23361  0cnop  23435  0cnfn  23436  idcnop  23437  lnopeq  23465  elunop2  23469  lnophm  23475  lnconi  23489  lnopcnbd  23492  lnfncnbd  23513  imaelshi  23514  riesz3i  23518  riesz4i  23519  riesz4  23520  riesz1  23521  cnlnadjlem2  23524  cnlnadjlem5  23527  cnlnadjlem8  23530  cnlnadji  23532  nmopadjlei  23544  cnvbraval  23566  leopg  23578  leoppos  23582  mdbr  23750  dmdbr  23755  cdj3i  23897  funcnv5mpt  24037  resspos  24140  isofld  24188  ofldadd  24191  ofldmul  24192  inftmrel  24203  isinftm  24204  rge0scvg  24288  qqhcn  24328  esumpcvgval  24421  sigaval  24446  issgon  24459  isrnmeas  24507  ismbfm  24555  isanmbfm  24559  mbfmcst  24562  sitgval  24600  ballotleme  24707  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem5  24770  lgambdd  24774  lgamcvglem  24777  derangenlem  24810  subfacp1lem3  24821  subfacp1lem5  24823  subfacp1lem6  24824  subfacp1  24825  erdszelem8  24837  kur14  24855  cnpcon  24870  rescon  24886  cvmscbv  24898  iscvm  24899  cvmsi  24905  cvmsval  24906  cvmlift3lem2  24960  snmlval  24971  ghomgrpilem1  25049  dedekind  25140  dedekindle  25141  dfpo2  25326  dfon2lem9  25361  dfrdg2  25366  dfrdg3  25367  poseq  25467  soseq  25468  wfrlem1  25470  wfrlem15  25484  frrlem1  25495  sltval  25515  nocvxminlem  25558  nobndlem2  25561  nobndlem8  25567  nobndup  25568  nobnddown  25569  brbtwn2  25748  colinearalg  25753  axsegconlem1  25760  axsegcon  25770  ax5seglem4  25775  ax5seglem5  25776  axlowdim  25804  axeuclidlem  25805  axcontlem1  25807  axcontlem2  25808  axcontlem4  25810  axcontlem5  25811  axcontlem8  25814  axcontlem12  25818  bpolylem  25998  bpolyval  25999  supaddc  26137  supadd  26138  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  voliunnfl  26149  volsupnfl  26150  mbfresfi  26152  itg2addnc  26158  nn0prpwlem  26215  isfne  26238  isfne4  26239  isfne2  26241  isfne3  26242  isref  26249  islocfin  26266  neibastop3  26281  topmeet  26283  topjoin  26284  filnetlem4  26300  f1opr  26316  upixp  26321  indexdom  26326  filbcmb  26332  sdclem2  26336  fdc  26339  lmclim2  26354  caures  26356  istotbnd  26368  istotbnd3  26370  sstotbnd  26374  isbnd  26379  heibor  26420  bfp  26423  rrncmslem  26431  exidres  26443  exidresid  26444  idlval  26513  isidl  26514  0idl  26525  unichnidl  26531  pridl  26537  ismaxidl  26540  smprngopr  26552  igenval2  26566  prnc  26567  ispridlc  26570  isnacs  26648  isnacs2  26650  nacsfix  26656  mzpclval  26672  elmzpcl  26673  rencldnfilem  26771  infmrgelbi  26831  pellfundre  26834  pellfundlb  26837  wepwsolem  27006  fnwe2lem2  27016  aomclem8  27027  dfac11  27028  frlmlbs  27117  gicabl  27131  islindf  27150  islinds2  27151  islindf2  27152  lindfrn  27159  lsslindf  27168  islindf4  27176  islnr3  27187  hbtlem2  27196  hbtlem5  27200  psgnunilem2  27286  psgnunilem3  27287  evth2f  27553  ubelsupr  27558  evthf  27565  fnchoice  27567  stoweidlem5  27621  stoweidlem9  27625  stoweidlem15  27631  stoweidlem16  27632  stoweidlem27  27643  stoweidlem28  27644  stoweidlem31  27647  stoweidlem34  27650  stoweidlem37  27653  stoweidlem46  27662  stoweidlem48  27664  stoweidlem51  27667  stoweidlem52  27668  stoweidlem59  27675  wallispilem3  27683  stirlinglem13  27702  cbvral2  27817  raaan2  27820  2reu4a  27834  dfdfat2  27862  frgrawopreg1  28153  frgrawopreg2  28154  bnj1185  28871  bnj1385  28910  bnj66  28937  bnj106  28945  bnj155  28956  bnj852  28998  bnj893  29005  bnj1228  29086  bnj1234  29088  bnj1463  29130  lubunNEW  29456  islfl  29543  eqlkr  29582  eqlkr3  29584  glbconN  29859  hlsuprexch  29863  ispsubsp  30227  ldilset  30591  isldil  30592  dilsetN  30635  isdilN  30636  trlset  30643  trlval  30644  cdleme27b  30850  cdleme29b  30857  cdleme31so  30861  cdleme31sn1  30863  cdleme31sn1c  30870  cdleme31fv  30872  cdleme40v  30951  istendo  31242  cdlemkid3N  31415  cdlemkid4  31416  cdlemkid5  31417  dihfval  31714  dihval  31715  islpolN  31966  hdmapffval  32312  hdmapfval  32313  hdmapval  32314  hdmapval2lem  32317  hgmapffval  32371  hgmapfval  32372  hgmapval  32373  hgmapvs  32377

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671