HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ralbidva 1651
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
StepHypRef Expression
1 ax-17 968 . 2 |- (ph -> A.xph)
2 ralbidva.1 . 2 |- ((ph /\ x e. A) -> (ps <-> ch))
31, 2ralbida 1649 1 |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   e. wcel 955  A.wral 1637
This theorem is referenced by:  disjssun 2316  ordunisssuc 3073  tfindsg2 3153  weinxp 3223  funimass3 3791  f1oweALT 3891  isfinite2 4523  kmlem2 4738  iscard 4825  axsup 5479  sup3 5999  infm3 6001  suprleub 6006  dfinfmr 6014  infmsup 6015  supxr2 6029  supxrre 6030  supxrbnd 6038  supxrbnd1 6042  supxrbnd2 6043  supxrleub 6046  zextltt 6137  primet 6142  shftf 6288  indstr 6393  fzshftralt 6454  cau2 6850  cvg1 6858  negfcncf 7204  acdcALT 7438  neips 7668  islp2 7688  cncnp 7717  cncnp2 7718  metreslem 7762  isopn4 7802  metcnplem 7825  metcnp2 7827  metcn 7828  metcnss 7837  lmbrf 7868  iscauf 7877  iscau5 7878  lmss 7888  causs 7890  metelcls 7900  metcn4 7905  cncms 7932  bcthlem33 7965  nvcni 8266  va1cnlem 8279  sm1cnilem 8281  nvcnpi4 8355  nmounbi 8371  isph 8412  phoeqi 8449  minveclem9 8484  minveclem24 8499  minveclem28 8503  h2hcau 8788  h2hlm 8789  hial2eq2t 8894  hcau2 8976  hhcms 8993  hhsscms 9067  hoeq1t 9673  hoeq2t 9674  adjsymt 9676  cnvadj 9733  hhlno 9743  leop2t 9969  leoptrit 9981  mdbr2 10133  dmdbr2 10140  mddmd 10144  cdj3lem3b 10272  cnvhmpha 10412
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972
This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1641
Copyright terms: Public domain