Theorem ralcom 1774

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 435	. . . . 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 1000	. . 3 |- (A.xA.y((x e. A /\ y e. B) -> ph) <-> A.xA.y((y e. B /\ x e. A) -> ph))
4		alcom 1032	. . 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 1676	. 2 |- (A.x e. A A.y e. B ph <-> A.xA.y((x e. A /\ y e. B) -> ph))
7		r2al 1676	. 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 954   e. wcel 958  A.wral 1645

This theorem is referenced by:  ralcom4 1823  ssint 2549  cnvpo 3522  cnvso 3523  fununi 3563  mapxpen 4495  cau3i 6914  fsumcom 7028  tgss3t 7638  basgen2t 7639  cncnp 7778  phoeqi 8518  occl 9181  ho02 9755  hoeq2t 9757  adjsymt 9759  cnvadj 9816  hhlno 9826  mddmd 10236  cdj3lem3b 10367

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

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

Copyright terms: Public domain