Theorem r19.26 1750

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 598	. . . 4 |- ((x e. A -> (ph /\ ps)) <-> ((x e. A -> ph) /\ (x e. A -> ps)))
2	1	albii 999	. . 3 |- (A.x(x e. A -> (ph /\ ps)) <-> A.x((x e. A -> ph) /\ (x e. A -> ps)))
3		19.26 1067	. . 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 1649	. 2 |- (A.x e. A (ph /\ ps) <-> A.x(x e. A -> (ph /\ ps)))
6		df-ral 1649	. . 3 |- (A.x e. A ph <-> A.x(x e. A -> ph))
7		df-ral 1649	. . 3 |- (A.x e. A ps <-> A.x(x e. A -> ps))
8	6, 7	anbi12i 482	. 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 954   e. wcel 958  A.wral 1645

This theorem is referenced by:  r19.26-2 1751  r19.35 1759  reu8 1936  ssrab 2125  r19.28zv 2350  r19.27zv 2353  iuneq2 2578  cnvpo 3522  fncnv 3561  fint 3650  abianfp 3962  ixpeq2 4355  xpmapenlem4 4499  xpmapenlem5 4500  aceq5 4740  ac5b 4753  kmlem6 4770  cvganz 6924  caubnd 6926  clm3 7079  climunii 7098  iserzshft2 7107  isummulc1 7212  isumcmpi 7215  infxpidmlem7 7558  tgval2t 7617  xplm 7975  xpcn 7976  hlimunii 9108  ocsh 9156  spanun 9467  adjvalvalt 9861  lnopcon 9963  lnfncon 9990  riesz4 9996  leopaddt 10065  leoptrit 10069  leoptrt 10070  chrelat4 10300  qusp 10555

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

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ral 1649

Copyright terms: Public domain