Theorem 2ralbidv 1727

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 1710	. 2 |- (ph -> (A.y e. B ps <-> A.y e. B ch))
3	2	ralbidv 1710	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 153  A.wral 1692

This theorem is referenced by:  cbvral3v 1851  poeq1 2898  soeq1 2909  isoeq1 3945  isoeq2 3946  isoeq3 3947  cau3iri 7005  cau5ii 7007  elcncf 7355  ismet 7883  ismsg 7885  msflem 7888  isgrp 8126  isabl 8185  isring 8225  ringi 8226  lnoval 8497  islno 8498  isphg 8560  ajmoi 8603  hcau 9134  projlem29 9297  adjmo 9841  elcnop 9866  ellnop 9867  elunop 9882  elhmop 9883  elcnfn 9892  ellnfn 9893  adjval 9897  adj1 9940  adjeq 9942  cnlnadjlem9 10091  cnlnadjeu 10094  cnlnssadj 10096  stel 10225  hstel 10226  cdj1i 10444  cdj3i 10452  elghomlem1 10467  elghomlem2 10468  isded 10751  dedi 10752  iscat 10769  cati 10770  ismona 10819  ismonb 10820  isepia 10829  isepib 10830  isfunb 10839

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232  df-ral 1696

Copyright terms: Public domain