Theorem rexeq1 1779

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 968	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 968	. 2 |- (y e. B -> A.x y e. B)
3	1, 2	rexeq1f 1776	1 |- (A = B -> (E.x e. A ph <-> E.x e. B ph))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953   e. wcel 955  E.wrex 1638

This theorem is referenced by:  rexeq1d 1782  rexeqd 1784  r19.12sn 2434  exss 2759  abrexexg 3846  oarec 4180  qseq1 4272  pssnn 4513  supeq1 4549  unbnnt 4611  bnd2 4696  aceq6b 4714  cflem 4877  cflecard 4884  cfeq0 4886  cfsuc 4887  elnp 5064  genpv 5074  xrsupsslem 6023  xrinfmsslem 6024  xrsupss 6025  xrinfmss 6026  cau5i 6854  cau4i 6855  cau5 6856  neifval 7655  cnpfval 7697  ishaus 7722  bcthlem29 7961  isgrp 7975  ch2 9035  pjtheu2 9165  pjpj0 9170  shsumvalt 9192  chne0t 9332  adjbdlnt 9931  subsp 10429

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465  df-rex 1642

Copyright terms: Public domain