Theorem r19.26 1742

Description: Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers.

Assertion

Ref	Expression
r19.26	|- (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ A.x e. A ps))

Proof of Theorem r19.26

Step	Hyp	Ref	Expression
1		jcab 596	. . . 4 |- ((x e. A -> (ph /\ ps)) <-> ((x e. A -> ph) /\ (x e. A -> ps)))
2	1	albii 996	. . 3 |- (A.x(x e. A -> (ph /\ ps)) <-> A.x((x e. A -> ph) /\ (x e. A -> ps)))
3		19.26 1063	. . 3 |- (A.x((x e. A -> ph) /\ (x e. A -> ps)) <-> (A.x(x e. A -> ph) /\ A.x(x e. A -> ps)))
4	2, 3	bitr 173	. 2 |- (A.x(x e. A -> (ph /\ ps)) <-> (A.x(x e. A -> ph) /\ A.x(x e. A -> ps)))
5		df-ral 1641	. 2 |- (A.x e. A (ph /\ ps) <-> A.x(x e. A -> (ph /\ ps)))
6		df-ral 1641	. . 3 |- (A.x e. A ph <-> A.x(x e. A -> ph))
7		df-ral 1641	. . 3 |- (A.x e. A ps <-> A.x(x e. A -> ps))
8	6, 7	anbi12i 481	. 2 |- ((A.x e. A ph /\ A.x e. A ps) <-> (A.x(x e. A -> ph) /\ A.x(x e. A -> ps)))
9	4, 5, 8	3bitr4 183	1 |- (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ A.x e. A ps))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 951   e. wcel 955  A.wral 1637

This theorem is referenced by:  r19.26-2 1743  r19.35 1751  reu8 1926  ssrab 2115  r19.28zv 2340  r19.27zv 2343  iuneq2 2568  cnvpo 3508  fncnv 3547  fint 3635  abianfp 3947  ixpeq2 4339  xpmapenlem4 4479  xpmapenlem5 4480  aceq5 4712  ac5b 4725  kmlem6 4742  cvganz 6861  caubnd 6863  clm3 7017  climunii 7035  iserzshft2 7044  isummulc1 7147  isumcmpi 7150  infxpidmlem7 7501  tgval2t 7559  xplm 7909  xpcn 7910  hlimunii 9029  ocsh 9072  spanun 9382  adjvalvalt 9777  lnopcon 9878  lnfncon 9905  riesz4 9911  leopaddt 9977  leoptrit 9981  chrelat4 10208  qusp 10430

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-or 224  df-an 225  df-ral 1641

Copyright terms: Public domain