Theorem ralbidv 2123

Description: Formula-building rule for restricted universal quantifier (deduction rule).

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

Proof of Theorem ralbidv

Step	Hyp	Ref	Expression
1		ax-17 1317	. 2 |- (ph -> A.xph)
2		ralbidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	ralbid 2121	1 |- (ph -> (A.x e. A ps <-> A.x e. A ch))

Syntax hints:   -> wi 3   <-> wb 163  A.wral 2105

This theorem is referenced by:  2ralbidv 2140  rexralbidv 2142  raleqbi1dv 2271  raleqbidv 2274  cbvral2v 2283  rcla42v 2384  rcla43v 2386  reu7 2447  sbcralt 2527  sbcralgf 2529  sbcralg 2531  raaan 2976  raaanv 2977  elintg 3222  elintrabg 3229  eliin 3260  iinab 3317  poeq1 3594  dffr2 3627  dffr2OLD 3628  wereu 3654  eufromeq1 3828  eufromeq2 3829  eufromeq3 3830  eufromeq5 3832  eufromeq6 3833  euobj1 3834  onssmin 3878  ralxpf 4043  cnvpo 4427  funcnvuni 4482  dff4 4791  dff13f 4851  isowe 4880  f1oweALT 4883  tfrlem3 5121  tfrlem12 5130  rdgeq1 5142  rdgeq2 5143  tz7.48lem 5164  elixp2 5408  ac6sfi 5509  riota5 5580  nneneq 5606  supeq1 5665  supmo 5666  supub 5670  suplub 5671  supmaxlem 5678  suppr 5680  supsnALT 5682  ordtypelem2 5685  ordtypelem6 5689  ordtypelem7 5690  ordtype 5691  zfregcl 5697  unbnn3 5746  rankval3 5792  unbndrank 5794  rankuni2 5801  rankun 5802  scottex 5846  scottexs 5848  scott0s 5849  bnd2 5854  hta 5858  aceq4 5896  aceq5lem5 5901  aceq5 5902  aceq6a 5903  aceq6b 5904  kmlem2 5928  kmlem13 5939  zorn2lem2 5951  zorn2lem7 5956  zorn2 5958  brdom3 5963  brdom7disj 5966  brdom6disj 5967  unidomg 5971  alephval2 6050  alephval3 6051  cflem 6053  cflecard 6060  cfeq0 6062  cfsuc 6063  nnleltp1 7138  lbreu 7254  lble 7256  lbinfm 7257  sup2 7260  infm3 7263  infmsup 7277  infmrcl 7278  xrsupsslem 7285  xrinfmsslem 7286  xrsupss 7287  xrinfmss 7288  supxr 7290  supxrre 7292  uzwo4OLD 7422  uzwo5OLD 7423  uzwo3lem2 7430  uzwo3 7431  zmax 7433  flval2 7478  flval3 7479  iccsupr 7567  uzwo 7624  uzwoOLD 7625  uzinfmi 7631  fsequb 7702  sqrlem6 7928  sqr2irrlem3 7976  seq1bndi 8162  cau3ii 8166  cau3iri 8167  cvg1 8173  cvg3i 8175  cvganz 8176  caubndi 8178  faclbnd4lem4 8203  bccl2 8223  clim 8237  csbfsum 8287  clm3i 8339  clm4i 8340  clm0i 8343  clm0nnsi 8345  clm4a 8350  climfnn 8352  climconsti 8354  climshfti 8364  climabs0i 8373  climaddlem3 8376  climmullem8 8387  climmulc2 8389  caucvglem2 8418  caucvglem5 8421  caucvg3 8428  serzf0i 8429  ser1clim0 8433  cvgcmp2lem 8440  cvgcmpubi 8446  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  cvgcmp3ce 8451  expcnvlem1 8488  expcnvlem6 8493  cncfval 8526  negfcncfi 8531  elcncf1di 8532  ivthlem8 8550  efaddlem25 8624  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  infpn2 8778  ruclem33 8811  cnfval 9032  cnpfval 9033  iscn 9034  cnpval 9035  iscnp 9036  iscnp2 9037  ismet 9075  ismsg 9077  msflem 9080  opnfval 9134  metcnp2 9166  metcnpi 9168  metcnpi2 9169  metcnpi3 9170  metcnpi4 9171  metcni 9172  metcni2 9173  metcnp3 9174  metcnss 9176  cncfmet 9183  lmfval 9203  caufval 9204  lmbr 9206  lmbrf 9208  lmconst 9212  lmnn 9213  iscau 9214  iscauf 9217  iscau5 9219  iscaunns 9222  lmss 9231  causs 9233  lmclim 9241  metcnp4 9248  metcn4i 9250  xplm 9253  xpcn 9254  iscms2lem4 9270  cncms 9276  isgrp 9321  isgrpi 9322  grpideu 9333  grpidinv2 9344  cnid 9435  mulid 9440  isgalem 9449  isring 9465  ringi 9466  ringideu 9470  cnring 9489  ringsn 9490  vci 9499  isvclem 9528  isnvlem 9561  nvi 9565  vacnlem3 9669  vacnlem4 9670  nmcnilem 9676  va1cnlem 9684  sm1cnilem 9686  lnoval 9752  islno 9753  nmobndi 9777  isblo3i 9801  blo3i 9802  blocnilem 9804  blocni 9805  ajfval 9809  isphg 9817  ubthlem1 9872  ubthlem14 9887  ubthi 9889  minveclem10 9899  minveclem39 9932  htthlem7 9973  spwval2 9996  spwmo 9999  spwpr2 10001  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  pilem2 10021  pilem3 10022  axgroth6 10137  oprabco 10159  indexfi 10174  fipreima 10175  homeofval 10234  ishomeo 10235  hmeobc 10239  isass 10363  exidu1 10373  cmpidelt 10376  h2hcau 10481  h2hlm 10482  hilid 10661  hcau 10684  hcau2 10688  hlimi 10689  hlim2 10693  hhcms 10705  sh 10711  hlim0 10738  ch2 10747  hhsscms 10783  ocel 10787  occllem8 10813  projlem8 10826  pjthi 10866  adjsym 11396  elcnop 11420  ellnop 11421  elcnfn 11446  ellnfn 11447  cnopc 11474  cnfnc 11491  adjvalval 11498  0cnop 11540  0cnfn 11541  idcnop 11542  lnopeq 11571  elunop2 11575  lnophm 11581  lnopconi 11600  lnopcon 11601  lnopcnbd 11602  lnfnconi 11627  lnfncon 11628  lnfncnbd 11629  riesz3i 11632  riesz4i 11633  riesz4 11634  riesz1 11635  cnlnadjlem2 11638  cnlnadjlem4 11640  cnlnadjlem5 11641  cnlnadjlem8 11644  cnlnadji 11646  nmopadjlei 11658  cnvbraval 11681  leopg 11693  leoppos 11697  stel 11786  mdbr 11866  dmdbr 11871  cdj3i 12013  bnj1185 12967  bnj1385 13102  bnj64 13201  bnj106 13225  bnj155 13246  bnj517 13259  bnj850 13312  bnj892 13322  bnj1228 13456  bnj1234 13460  bnj1463 13550  bnj1482 13551  ralbieq1dvOLD 13583  ghomgrpilem1 13628  ublbneg 13653  lbzbi 13657  gcdcllem1 13718  gcdcllem2 13719  dfon2lem9 13857  frxp 13951  poseq 13954  soseq 13955  wfrlem1 13957  wfrlem15 13971  sltval 13988  nocvxminlem 14028  axfelem1 14031  axfelem7 14037  axfelem8 14038  axfelem9 14039  axfelem15 14045  axfelem16 14046  inpreima5 14469  elixp2b 14494  prjmapcp2 14515  islatalg 14531  ubos2 14598  ubos 14599  puub2 14600  puub 14601  supdef 14604  ismxl2 14609  ismnl2 14610  mnlmxl2 14611  defge3 14613  defse3 14614  clfsebs 14707  clfsebsr 14709  clfsebs2 14710  symgfo 14730  curgrpact 14735  fprodneg 14741  fprodsub 14742  ununr 14769  vecval1b 14794  vecval3b 14795  vri 14834  cnvhmphb 14880  cnvhmph 14881  hmeogrp 14892  usptoplem 14917  istopx 14918  prtoptop 14919  usptop 14920  idtrgrp 14978  isded 15083  dedi 15084  iscat 15101  cati 15102  ismona 15158  isepia 15168  isfunb 15183  isplibg3 15313  isplibg4a 15315  isplibg4b 15317  ordtypelem2OLD 15376  ordtypelem6OLD 15380  ordtypelem7OLD 15381  ordtypeOLD 15382  alexsublem3 15439  1stcclb 15471  2ndc1stc 15477  isfne 15480  isref 15488  islocfin 15506  topmeet 15526  topjoin 15527  fnemeet1 15528  fnemeet2 15529  ufileu 15573  uffixfr 15575  limfilcf 15587  flimfbas 15601  fclusnei 15607  fclusbas 15610  fcluscf 15612  fclusfnei 15626  f1opr 15714  upixp 15729  fimax 15746  indexdom 15754  indexfiOLD 15755  fipreimaOLD 15756  zornn0 15764  frfi 15771  frminex 15773  filbcmb 15776  sdc 15811  fdc 15812  iserzshft2 15829  caushft 15851  metdcn 15853  tlmbr 15904  istotbnd 15933  sstotbnd 15936  totbndss 15937  totbndbnd 15944  heiborlem16 15970  heiborlem18 15972  heiborlem23 15977  bfp 16009  exidres 16031  exidresid 16032  isgrpda 16033  phtpyval 16047  isphtpy 16048  isringd 16097  idlval 16161  isidl 16162  0idl 16173  unichnidl 16179  pridl 16185  ismaxidl 16188  smprngpr 16200  igenval2 16214  prnc 16215  ispridlc 16218  smoeq 16444  eustrdif 16722  stbval 16731  isposNEW 16773  lubfval 16803  lubval 16804  lubprop 16805  lubid 16807  glbfval 16808  glbval 16809  glbprop 16810  glbvalle 16811  glbprople 16812  joinval2 16816  joinlem 16817  meetval2 16823  meetlem 16824  lubl 16896  lubun 16899  lubunNEW 16900  clatleglb 16903  glbcon 17028  hlsuprexch 17033  isgrpNEW 17104  grpideuNEW 17114  isgrpiNEW 17115  grpidinv2NEW 17119  isringNEW 17142  ringideuNEW 17146  ringidmlemNEW 17153  isphil 17195  ocvfval 17206  ispsubsp 17226  dilset 17402  isdil 17403

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ral 2109

Copyright terms: Public domain