Theorem r2al 1673

Description: Double restricted universal quantification.

Assertion

Ref	Expression
r2al	|- (A.x e. A A.y e. B ph <-> A.xA.y((x e. A /\ y e. B) -> ph))

Distinct variable groups:   x,y   y,A

Proof of Theorem r2al

Step	Hyp	Ref	Expression
1		df-ral 1646	. 2 |- (A.x e. A A.y e. B ph <-> A.x(x e. A -> A.y e. B ph))
2		19.21v 1283	. . . 4 |- (A.y(x e. A -> (y e. B -> ph)) <-> (x e. A -> A.y(y e. B -> ph)))
3		impexp 347	. . . . 5 |- (((x e. A /\ y e. B) -> ph) <-> (x e. A -> (y e. B -> ph)))
4	3	albii 997	. . . 4 |- (A.y((x e. A /\ y e. B) -> ph) <-> A.y(x e. A -> (y e. B -> ph)))
5		df-ral 1646	. . . . 5 |- (A.y e. B ph <-> A.y(y e. B -> ph))
6	5	imbi2i 185	. . . 4 |- ((x e. A -> A.y e. B ph) <-> (x e. A -> A.y(y e. B -> ph)))
7	2, 4, 6	3bitr4 183	. . 3 |- (A.y((x e. A /\ y e. B) -> ph) <-> (x e. A -> A.y e. B ph))
8	7	albii 997	. 2 |- (A.xA.y((x e. A /\ y e. B) -> ph) <-> A.x(x e. A -> A.y e. B ph))
9	1, 8	bitr4 176	1 |- (A.x e. A A.y e. B ph <-> A.xA.y((x e. A /\ y e. B) -> ph))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 952   e. wcel 956  A.wral 1642

This theorem is referenced by:  r3al 1687  ralcom 1771  soss 2847  dfwe2 2930  weinxp 3228  fununi 3555  f1fv 3865  tz7.48lem 3946  tz7.49 3950  inf3lem6 4598  zorn2lem4 4771  zorn2lem6 4773  projlem28 9152  imonclem 10619  ismonc 10620

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976

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

Copyright terms: Public domain