Theorem raleq1d 1792

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 1789	. 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 958  A.wral 1648

This theorem is referenced by:  raleq12d 1797  cbvfo 3891  zorn2lem6 4803  zorn2lem7 4804  zorn2 4806  fzrevral2t 6521  fzrevral3t 6522  fzshftralt 6523  fsequb 6524  seqzfveq 6555  fsumcllem 7014  fsum1ps 7018  fsumadd 7022  fsumcom 7028  fsumrev 7029  fsummulc1 7033  fsumcmp 7040  fsumcmpndx2 7042  fsumabs 7043  clm4at 7090  fsum0diag 7258  metcn 7886  metcn4 7968  isring 8137  ringi 8138  nvcni 8325  nvcni2 8326  nvcnpi3 8418  nvcnpi4 8419  iscat 10658  cati 10659  ismona 10708  isepia 10718

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-cleq 1472  df-clel 1475  df-ral 1652

Copyright terms: Public domain