Theorem raleqd 1790

Description: Equality deduction for restricted universal quantifier.

Hypothesis

Ref	Expression
raleqd.1	|- (A = B -> (ph <-> ps))

Assertion

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

Distinct variable groups:   x,A   x,B

Proof of Theorem raleqd

Step	Hyp	Ref	Expression
1		raleq1 1785	. 2 |- (A = B -> (A.x e. A ph <-> A.x e. B ph))
2		raleqd.1	. . 3 |- (A = B -> (ph <-> ps))
3	2	ralbidv 1662	. 2 |- (A = B -> (A.x e. B ph <-> A.x e. B ps))
4	1, 3	bitrd 528	1 |- (A = B -> (A.x e. A ph <-> A.x e. B ps))

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

This theorem is referenced by:  isoeq4 3888  dfom3 4618  aceq1 4717  aceq5lem4 4726  kmlem1 4753  kmlem10 4762  kmlem13 4765  kmlem14 4766  elnp 5080  peano5nn 5894  dfnn2 5904  dfuz 6170  peano5uz 6171  cncfval 7222  istopg 7553  isbasisg 7568  basis2t 7572  eltg2t 7576  basgen2t 7596  ismet 7755  dfms2 7756  ismsg 7757  msflem 7760  metreslem 7779  isopn 7816  isgrp 7998  isabl 8058  ringi 8099  sh 9033  iseuctopg 10444  isfil 10488

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 1648

Copyright terms: Public domain