Theorem raleq1 1778

Description: Equality theorem for restricted universal quantifier.

Assertion

Ref	Expression
raleq1	|- (A = B -> (A.x e. A ph <-> A.x e. B ph))

Distinct variable groups:   x,A   x,B

Proof of Theorem raleq1

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 968	. 2 |- (y e. B -> A.x y e. B)
3	1, 2	raleq1f 1775	1 |- (A = B -> (A.x e. A ph <-> A.x e. B ph))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953   e. wcel 955  A.wral 1637

This theorem is referenced by:  raleq1d 1781  raleqd 1783  sbralie 1931  inteq 2526  iineq1 2566  fri 2908  tfis 3117  tfinds 3151  fncnv 3547  cbvfo 3870  isoeq4 3875  f1oweALT 3891  tfrlem1 3896  tfrlem3 3898  tfrlem12 3907  ixpeq1 4337  unifi 4532  supeq1 4549  bnd2 4696  aceq3lem 4704  aceq5lem4 4710  aceq5 4712  ac4c 4723  ac5 4724  kmlem1 4737  kmlem10 4746  kmlem12 4748  kmlem13 4749  zorn2lem7 4766  zorn2 4768  unidomg 4781  cfval 4878  xrsupsslem 6023  xrinfmsslem 6024  xrsupss 6025  xrinfmss 6026  cau4i 6855  cau5 6856  clmnns 7022  isumnn0nn 7142  infcvglem3 7158  cncfval 7199  acdc3lem 7428  acdc3 7429  acdc2lem1 7430  acdc2 7432  acdc5lem1 7433  acdc5 7435  acdclem 7436  acdc 7437  basgen2t 7581  cnfval 7696  cnpfval 7697  ismet 7737  dfms2 7738  ismsg 7739  msflem 7742  metreslem 7762  isgrp 7975  isabl 8037  ringi 8079  minveclem30 8505  spwval2 8577  spwval 8582  ocvalt 9069  cdj3lem3b 10272  elghom 10289  homeofval 10403

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465  df-ral 1641

Copyright terms: Public domain