Theorem cla4egv 1863

Description: Existential specialization with implicit substitution.

Hypothesis

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

Assertion

Ref	Expression
cla4egv	|- (A e. B -> (ps -> E.xph))

Distinct variable groups:   ps,x   x,A

Proof of Theorem cla4egv

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 971	. 2 |- (ps -> A.xps)
3		cla4gv.1	. 2 |- (x = A -> (ph <-> ps))
4	1, 2, 3	cla4egf 1861	1 |- (A e. B -> (ps -> E.xph))

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

This theorem is referenced by:  cla4ev 1869  elunii 2508  opeldm 3314  unielxp 4107  enrefg 4390  f1oen2g 4394  f1domg 4396  fodomr 4483  unfilem3 4550  fodomfiOLD 4566  infeq5 4621  oncard 4829  cardsn 4834  cflem 4905  cflecard 4912  ltexpri 5149  recexpr 5160  supexpr 5163  infi1 10447  infi1OLD 10448  fine 10449  fineOLD 10450  hmphsyma 10528  hmphre 10530  hmphtr 10531  homcard 10539  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem5 10593  rcfpfillem5OLD 10594

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