Theorem rexeq1 1787

Description: Equality theorem for restricted existential quantifier.

Assertion

Ref	Expression
rexeq1	|- (A = B -> (E.x e. A ph <-> E.x e. B ph))

Distinct variable groups:   x,A   x,B

Proof of Theorem rexeq1

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 971	. 2 |- (y e. B -> A.x y e. B)
3	1, 2	rexeq1f 1784	1 |- (A = B -> (E.x e. A ph <-> E.x e. B ph))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956   e. wcel 958  E.wrex 1646

This theorem is referenced by:  rexeq1d 1790  rexeqd 1792  r19.12sn 2444  exss 2769  abrexexg 3861  oarec 4196  qseq1 4288  pssnn 4534  supeq1 4575  unbnnt 4639  bnd2 4724  aceq6b 4742  cflem 4905  cflecard 4912  cfeq0 4914  cfsuc 4915  elnp 5092  genpv 5102  xrsupsslem 6076  xrinfmsslem 6077  xrsupss 6078  xrinfmss 6079  cau5i 6917  cau4i 6918  cau5 6919  neifval 7714  cnpfval 7757  ishaus 7783  bcthlem29 8027  isgrp 8041  ch2 9114  pjtheu2 9250  pjpj0 9255  shsumvalt 9277  chne0t 9417  adjbdlnt 10016  subsp 10554

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-rex 1650

Copyright terms: Public domain