Theorem 2ralbidv 1683

Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Distinct variable restriction on x and y removed by Szymon Jaroszewicz, 16-Mar-2006.)

Hypothesis

Ref	Expression
2ralbidv.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
2ralbidv	|- (ph -> (A.x e. A A.y e. B ps <-> A.x e. A A.y e. B ch))

Distinct variable groups:   ph,x   ph,y

Proof of Theorem 2ralbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 |- (ph -> (ps <-> ch))
2	1	ralbidv 1666	. 2 |- (ph -> (A.y e. B ps <-> A.y e. B ch))
3	2	ralbidv 1666	1 |- (ph -> (A.x e. A A.y e. B ps <-> A.x e. A A.y e. B ch))

Syntax hints:   -> wi 3   <-> wb 146  A.wral 1648

This theorem is referenced by:  cbvral3v 1807  poeq1 2848  soeq1 2859  isoeq1 3893  isoeq2 3894  isoeq3 3895  cau3ir 6915  cau5i 6917  elcncf 7265  ismet 7795  ismsg 7797  msflem 7800  isgrp 8038  isabl 8097  isring 8137  ringi 8138  lnoval 8409  islno 8410  isphg 8472  ajmoi 8515  hcau 9046  projlem29 9209  adjmo 9753  elcnopt 9778  ellnopt 9779  elunopt 9794  elhmopt 9795  elcnfnt 9804  ellnfnt 9805  adjvalt 9809  adjt 9852  adjeqt 9854  cnlnadjlem9 10003  cnlnadjeut 10006  cnlnssadj 10008  stelt 10136  hstelt 10137  cdj1 10355  cdj3 10363  elghomlem1 10377  elghomlem2 10378  isded 10640  dedi 10641  iscat 10658  cati 10659  ismona 10708  ismonb 10709  isepia 10718  isepib 10719  isfunb 10726

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

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

Copyright terms: Public domain