Theorem ceqsexgv 1888

Description: Elimination of an existential quantifier, using implicit substitution.

Hypothesis

Ref	Expression
ceqsexgv.1	|- (x = A -> (ph <-> ps))

Assertion

Ref	Expression
ceqsexgv	|- (A e. B -> (E.x(x = A /\ ph) <-> ps))

Distinct variable groups:   x,A   ps,x

Proof of Theorem ceqsexgv

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (ps -> A.xps)
2		ceqsexgv.1	. 2 |- (x = A -> (ph <-> ps))
3	1, 2	ceqsexg 1887	1 |- (A e. B -> (E.x(x = A /\ ph) <-> ps))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958  E.wex 980

This theorem is referenced by:  ceqsrexv 1889  clel3g 1892  imasng 3424  elxp5 3454  fvopabn 3786  2ndconst 4097  xpsnen 4435  ismet 7798  isgrp 8041  spwval2 8653  bsi 10495  rcfpfillem3 10589  rcfpfillem3OLD 10590

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-8 964  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain