Theorem ralbidva 1662

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

Hypothesis

Ref	Expression
ralbidva.1	|- ((ph /\ x e. A) -> (ps <-> ch))

Assertion

Ref	Expression
ralbidva	|- (ph -> (A.x e. A ps <-> A.x e. A ch))

Distinct variable group:   ph,x

Proof of Theorem ralbidva

Step	Hyp	Ref	Expression
1		ax-17 973	. 2 |- (ph -> A.xph)
2		ralbidva.1	. 2 |- ((ph /\ x e. A) -> (ps <-> ch))
3	1, 2	ralbida 1660	1 |- (ph -> (A.x e. A ps <-> A.x e. A ch))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   e. wcel 960  A.wral 1648

This theorem is referenced by:  disjssun 2330  ordunisssuc 3089  tfindsg2 3169  weinxp 3239  funimass3 3812  f1oweALT 3912  isfinite2 4557  isfinite2OLD 4558  kmlem2 4776  iscard 4864  axsup 5519  sup3 6054  infm3 6056  suprleub 6061  dfinfmr 6069  infmsup 6070  supxr2 6084  supxrre 6085  supxrbnd 6093  supxrbnd1 6097  supxrbnd2 6098  supxrleub 6101  zextltt 6192  primet 6197  shftf 6352  indstr 6462  fzshftralt 6523  cau2 6913  cvg1 6921  negfcncf 7269  acdcALT 7497  neips 7724  islp2 7744  cncnp 7775  cncnp2 7776  metreslem 7819  isopn4 7859  metcnplem 7883  metcnp2 7885  metcn 7886  metcnss 7895  lmbrf 7927  iscauf 7936  iscau5 7938  iscaunns 7941  lmss 7950  causs 7952  metelcls 7962  metcn4 7968  cncms 7995  bcthlem33 8028  nvcni 8325  nvcni2 8326  nvcni3 8327  va1cnlem 8341  sm1cnilem 8343  nvcnpi3 8418  nvcnpi4 8419  nmounbi 8435  isph 8477  phoeqi 8514  minveclem9 8549  minveclem24 8564  minveclem28 8568  h2hcau 8844  h2hlm 8845  hial2eq2t 8968  hcau2 9050  hhcms 9067  hhsscms 9145  projlemHIL 9213  hoeq1t 9751  hoeq2t 9752  adjsymt 9754  cnvadj 9811  hhlno 9821  leop2t 10052  leoptrit 10064  mdbr2 10218  dmdbr2 10225  mddmd 10231  cdj3lem3b 10362  cnvhmpha 10511

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1652

Copyright terms: Public domain