Theorem cla4egv 1866

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 973	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 973	. 2 |- (ps -> A.xps)
3		cla4gv.1	. 2 |- (x = A -> (ph <-> ps))
4	1, 2, 3	cla4egf 1864	1 |- (A e. B -> (ps -> E.xph))

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

This theorem is referenced by:  cla4ev 1872  elunii 2512  opeldm 3320  unielxp 4113  enrefg 4396  f1oen2g 4400  f1domg 4402  fodomr 4489  unfilem3 4562  fodomfi 4575  fodomfiOLD 4576  infeq5 4630  oncard 4839  cardsn 4844  cflem 4917  cflecard 4924  ltexpri 5161  recexpr 5172  supexpr 5175  infi1 10441  fine 10442  hmphsyma 10514  hmphre 10516  hmphtr 10517  homcard 10525  rcfpfillem3 10565  rcfpfillem5 10567

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-8 966  ax-12 970  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-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815

Copyright terms: Public domain