Theorem ralbidv2 2892

Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.)

Hypothesis

Ref	Expression
ralbidv2.1

Assertion

Ref	Expression
ralbidv2

Distinct variable group:   ,

Proof of Theorem ralbidv2

Step	Hyp	Ref	Expression
1		ralbidv2.1	. . 3
2	1	albidv 1713	. 2
3		df-ral 2812	. 2
4		df-ral 2812	. 2
5	2, 3, 4	3bitr4g 288	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  e.wcel 1818  A.wral 2807

This theorem is referenced by:  ralbidva  2893  ralss  3565  oneqmini  4934  ordunisuc2  6679  dfsmo2  7037  wemapsolem  7996  zorn2lem1  8897  raluz  11158  limsupgle  13300  ello12  13339  elo12  13350  lo1resb  13387  rlimresb  13388  o1resb  13389  isprm3  14226  ist1  19822  ist1-2  19848  hausdiag  20146  xkopt  20156  cnflf  20503  cnfcf  20543  metcnp  21044  caucfil  21722  mdegleb  22464  eulerpartlemgvv  28315  filnetlem4  30199  isprm7  31192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704

This theorem depends on definitions:  df-bi 185  df-ral 2812