Theorem rexeq1 1790

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

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

This theorem is referenced by:  rexeq1d 1793  rexeqd 1795  r19.12sn 2448  exss 2775  abrexexg 3867  oarec 4202  qseq1 4294  pssnn 4544  supeq1 4584  unbnnt 4649  bnd2 4734  aceq6b 4752  cflem 4917  cflecard 4924  cfeq0 4926  cfsuc 4927  elnp 5104  genpv 5114  xrsupsslem 6078  xrinfmsslem 6079  xrsupss 6080  xrinfmss 6081  cau5i 6917  cau4i 6918  cau5 6919  neifval 7711  cnpfval 7754  ishaus 7780  bcthlem29 8024  isgrp 8038  ch2 9109  pjtheu2 9245  pjpj0 9250  shsumvalt 9272  chne0t 9412  adjbdlnt 10011  subsp 10540

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

Copyright terms: Public domain