Theorem 2ralbidv 1680

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 1663	. 2 |- (ph -> (A.y e. B ps <-> A.y e. B ch))
3	2	ralbidv 1663	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 1645

This theorem is referenced by:  cbvral3v 1804  poeq1 2842  soeq1 2853  isoeq1 3887  isoeq2 3888  isoeq3 3889  cau3ir 6915  cau5i 6917  elcncf 7265  ismet 7798  ismsg 7800  msflem 7803  isgrp 8041  isabl 8101  isring 8141  ringi 8142  lnoval 8413  islno 8414  isphg 8476  ajmoi 8519  hcau 9051  projlem29 9214  adjmo 9758  elcnopt 9783  ellnopt 9784  elunopt 9799  elhmopt 9800  elcnfnt 9809  ellnfnt 9810  adjvalt 9814  adjt 9857  adjeqt 9859  cnlnadjlem9 10008  cnlnadjeut 10011  cnlnssadj 10013  stelt 10141  hstelt 10142  cdj1 10360  cdj3 10368  elghomlem1 10382  elghomlem2 10383  isded 10669  dedi 10670  iscat 10687  cati 10688  ismona 10737  ismonb 10738  isepia 10747  isepib 10748  isfunb 10755

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

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

Copyright terms: Public domain