Theorem biraldv 1219

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

Hypothesis

Ref	Expression
biraldv.1	|- (ph -> (ps <-> ch))

Assertion

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

Distinct variable group(s):   ph,x

Proof of Theorem biraldv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ph -> A.xph)
2		biraldv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	birald 1217	1 |- (ph -> (A.x e. A ps <-> A.x e. A ch))

Syntax hints:   -> wi 2   <-> wb 127  A.wral 1201

This theorem is referenced by:  raleqd 1327  cbvral2v 1336  rcla42v 1404  raaan 1775  elintg 1973  eliin 1999  poeq1 2130  soeq1 2141  supeq1 2155  supmo 2156  supub 2160  suplub 2161  supsn 2168  dffr2 2171  freq1 2174  wereu 2197  onssmin 2263  funcnvuni 2706  f1fvf 2917  isoeq1 2925  isoeq2 2926  isoeq3 2927  isowe 2941  f1oweOLD 2944  tfrlem3 2951  tfrlem12 2960  rdgeq1 2972  rdgeq2 2973  tz7.48lem 2993  nneneq 3408  fiint 3445  zfregcl 3446  rankval3 3525  unbndrank 3527  rankuni 3533  rankun 3535  scottex 3541  scottexs 3543  scott0s 3544  bnd2 3549  aceq4 3557  aceq5lem5 3562  aceq5 3563  aceq6a 3564  aceq6b 3565  kmlem2 3581  kmlem12 3591  zornlem2 3604  zornlem7 3609  zorn 3611  hta 3619  cflem 3700  cflecard 3707  cfsuc 3709  nnleltp1t 4448  sup2 4510  uzwo 4605  uzwo2 4606  nnwoOLD 4608  uzwo3lem2 4615  uzwo3 4616  zmax 4618  sqrlem6 4736  sqr2irrlem3 4779  clim 4877  clim2 4881  clim0 4882  climunii 4883  ruclem33 4917  hcauchy 5103  hlim 5108  hlim2 5112  sh 5116  hlim0 5140  hlimcaui 5141  hlimunii 5143  ch2 5149  ocelt 5162  occllem6 5185  occllem8 5187  projlem8 5200  projlem29 5221  pjth 5239  stelt 5671  mdbr 5726

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ral 1205

metamath.org