Theorem ralbid 2121

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

Hypotheses

Ref	Expression
ralbid.1	|- (ph -> A.xph)
ralbid.2	|- (ph -> (ps <-> ch))

Assertion

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

Proof of Theorem ralbid

Step	Hyp	Ref	Expression
1		ralbid.1	. 2 |- (ph -> A.xph)
2		ralbid.2	. . 3 |- (ph -> (ps <-> ch))
3	2	adantr 425	. 2 |- ((ph /\ x e. A) -> (ps <-> ch))
4	1, 3	ralbida 2117	1 |- (ph -> (A.x e. A ps <-> A.x e. A ch))

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296   e. wcel 1300  A.wral 2105

This theorem is referenced by:  ralbidv 2123  ralbii 2127  sbcralt 2527  sbcrext 2528  sbcralgf 2529  sbcrexgf 2530  eufromeq2 3829  eufromeq6 3833  euobj1 3834  zfrep6 4545  ordtypelem6 5689  cplem2 5851  ac6lem 5916  lble 7256  irred 11967  unprj 14511  svli2 14826  ordtypelem6OLD 15380  neibastop2lem4 15522  neibastop3 15524  indexa 15753  fsumleisumi 15826

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ral 2109

Copyright terms: Public domain