Theorem raleq1d 1789

Description: Equality deduction for restricted universal quantifier.

Hypothesis

Ref	Expression
raleq1d.1	|- (ph -> A = B)

Assertion

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

Distinct variable groups:   x,A   x,B

Proof of Theorem raleq1d

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 |- (ph -> A = B)
2		raleq1 1786	. 2 |- (A = B -> (A.x e. A ps <-> A.x e. B ps))
3	1, 2	syl 10	1 |- (ph -> (A.x e. A ps <-> A.x e. B ps))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956  A.wral 1645

This theorem is referenced by:  raleq12d 1794  cbvfo 3885  zorn2lem6 4793  zorn2lem7 4794  zorn2 4796  fzrevral2t 6520  fzrevral3t 6521  fzshftralt 6522  fsequb 6523  seqzfveq 6554  fsumcllem 7014  fsum1ps 7018  fsumadd 7022  fsumcom 7028  fsumrev 7029  fsummulc1 7033  fsumcmp 7040  fsumcmpndx2 7042  fsumabs 7043  clm4at 7090  fsum0diag 7258  metcn 7889  metcn4 7971  isring 8141  ringi 8142  nvcni 8329  nvcni2 8330  nvcnpi3 8422  nvcnpi4 8423  iscat 10687  cati 10688  ismona 10737  isepia 10747

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472  df-ral 1649

Copyright terms: Public domain