Theorem ralcom 1777

Description: Commutation of restricted quantifiers.

Assertion

Ref	Expression
ralcom	|- (A.x e. A A.y e. B ph <-> A.y e. B A.x e. A ph)

Distinct variable groups:   x,y   x,B   y,A

Proof of Theorem ralcom

Step	Hyp	Ref	Expression
1		ancom 437	. . . . 5 |- ((x e. A /\ y e. B) <-> (y e. B /\ x e. A))
2	1	imbi1i 186	. . . 4 |- (((x e. A /\ y e. B) -> ph) <-> ((y e. B /\ x e. A) -> ph))
3	2	2albii 1002	. . 3 |- (A.xA.y((x e. A /\ y e. B) -> ph) <-> A.xA.y((y e. B /\ x e. A) -> ph))
4		alcom 1034	. . 3 |- (A.xA.y((y e. B /\ x e. A) -> ph) <-> A.yA.x((y e. B /\ x e. A) -> ph))
5	3, 4	bitr 173	. 2 |- (A.xA.y((x e. A /\ y e. B) -> ph) <-> A.yA.x((y e. B /\ x e. A) -> ph))
6		r2al 1679	. 2 |- (A.x e. A A.y e. B ph <-> A.xA.y((x e. A /\ y e. B) -> ph))
7		r2al 1679	. 2 |- (A.y e. B A.x e. A ph <-> A.yA.x((y e. B /\ x e. A) -> ph))
8	5, 6, 7	3bitr4 183	1 |- (A.x e. A A.y e. B ph <-> A.y e. B A.x e. A ph)

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

This theorem is referenced by:  ralcom4 1826  ssint 2553  cnvpo 3528  cnvso 3529  fununi 3569  mapxpen 4501  cau3i 6914  fsumcom 7028  tgss3t 7637  basgen2t 7638  cncnp 7775  phoeqi 8514  occl 9176  ho02 9750  hoeq2t 9752  adjsymt 9754  cnvadj 9811  hhlno 9821  mddmd 10231  cdj3lem3b 10362

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980

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

Copyright terms: Public domain