Theorem raleqd 1791

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 1786	. 2 |- (A = B -> (A.x e. A ph <-> A.x e. B ph))
2		raleqd.1	. . 3 |- (A = B -> (ph <-> ps))
3	2	ralbidv 1663	. 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 1645

This theorem is referenced by:  isoeq4 3890  dfom3 4630  aceq1 4729  aceq5lem4 4738  kmlem1 4765  kmlem10 4774  kmlem13 4777  kmlem14 4778  elnp 5092  peano5nn 5926  dfnn2 5936  dfuz 6202  peano5uz 6203  cncfval 7264  istopg 7596  isbasisg 7611  basis2t 7615  eltg2t 7619  basgen2t 7639  ismet 7798  dfms2 7799  ismsg 7800  msflem 7803  metreslem 7822  isopn 7859  isgrp 8041  isabl 8101  ringi 8142  sh 9078  iseuctopg 10502  isfil 10558

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