Theorem ralbidv2 1665

Description: Formula-building rule for restricted universal quantifier (deduction rule).

Hypothesis

Ref	Expression
ralbidv2.1	|- (ph -> ((x e. A -> ps) <-> (x e. B -> ch)))

Assertion

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

Distinct variable group:   ph,x

Proof of Theorem ralbidv2

Step	Hyp	Ref	Expression
1		ralbidv2.1	. . 3 |- (ph -> ((x e. A -> ps) <-> (x e. B -> ch)))
2	1	albidv 1278	. 2 |- (ph -> (A.x(x e. A -> ps) <-> A.x(x e. B -> ch)))
3		df-ral 1649	. 2 |- (A.x e. A ps <-> A.x(x e. A -> ps))
4		df-ral 1649	. 2 |- (A.x e. B ch <-> A.x(x e. B -> ch))
5	2, 3, 4	3bitr4g 555	1 |- (ph -> (A.x e. A ps <-> A.x e. B ch))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954   e. wcel 958  A.wral 1645

This theorem is referenced by:  oneqmini 3017  ordunisuc2 3115  oaabs 4252  zorn2lem1 4788  iscard2 4854  supxrre 6083  raluz 6442  efcn 7423  metcnplem 7886  cncfmet 7905  ist1 10614  isded 10669  dedi 10670  iscat 10687  cati 10688  isfuna 10754

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