Theorem raleqd 1794

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 1789	. 2 |- (A = B -> (A.x e. A ph <-> A.x e. B ph))
2		raleqd.1	. . 3 |- (A = B -> (ph <-> ps))
3	2	ralbidv 1666	. 2 |- (A = B -> (A.x e. B ph <-> A.x e. B ps))
4	1, 3	bitrd 530	1 |- (A = B -> (A.x e. A ph <-> A.x e. B ps))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 958  A.wral 1648

This theorem is referenced by:  isoeq4 3896  dfom3 4639  aceq1 4739  aceq5lem4 4748  kmlem1 4775  kmlem10 4784  kmlem13 4787  kmlem14 4788  elnp 5104  peano5nn 5928  dfnn2 5938  dfuz 6204  peano5uz 6205  cncfval 7264  istopg 7598  isbasisg 7610  basis2t 7614  eltg2t 7618  basgen2t 7638  ismet 7795  dfms2 7796  ismsg 7797  msflem 7800  metreslem 7819  isopn 7856  isgrp 8038  isabl 8097  ringi 8138  sh 9073  iseuctopg 10488  isfil 10544

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