HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem r19.20i2 1695
Description: Inference quantifying both antecedent and consequent.
Hypothesis
Ref Expression
r19.20i2.1 |- ((x e. A -> ph) -> (x e. B -> ps))
Assertion
Ref Expression
r19.20i2 |- (A.x e. A ph -> A.x e. B ps)
Proof of Theorem r19.20i2
StepHypRef Expression
1 r19.20i2.1 . . 3 |- ((x e. A -> ph) -> (x e. B -> ps))
2119.20i 989 . 2 |- (A.x(x e. A -> ph) -> A.x(x e. B -> ps))
3 df-ral 1641 . 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
4 df-ral 1641 . 2 |- (A.x e. B ps <-> A.x(x e. B -> ps))
52, 3, 43imtr4 219 1 |- (A.x e. A ph -> A.x e. B ps)
Colors of variables: wff set class
Syntax hints:   -> wi 3  A.wal 951   e. wcel 955  A.wral 1637
This theorem is referenced by:  r19.20i 1696  ralcom3 1769  tfi 3116  omex 4599  kmlem1 4737  brdom5 4774  brdom4 4775  xrub 6027  seqzeq 6487  cau5i 6854  iserzshft2 7044  clim2serzt 7070  iserzmulc1 7072  isum1p 7141  isumreclt 7145  isummulc1ALT 7148  fsum0diaglem2 7192  basgen2t 7581  sumdmd 10254  dmdbr6at 10256
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972
This theorem depends on definitions:  df-bi 147  df-ral 1641
Copyright terms: Public domain