Theorem cla4egv 1397

Description: Existential specialization with implicit substitution.

Hypothesis

Ref	Expression
cla4gv.1	⊢ (x = A → (φ ↔ ψ))

Assertion

Ref	Expression
cla4egv	⊢ (A ∈ B → (ψ → ∃xφ))

Distinct variable group(s):   ψ,x   x,A

Proof of Theorem cla4egv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 ⊢ (y ∈ A → ∀x y ∈ A)
2		ax-17 925	. 2 ⊢ (ψ → ∀xψ)
3		cla4gv.1	. 2 ⊢ (x = A → (φ ↔ ψ))
4	1, 2, 3	cla4egf 1395	1 ⊢ (A ∈ B → (ψ → ∃xφ))

Syntax hints:   → wi 2   ↔ wb 127  ∃wex 678   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  rcla4ev 1403  elunii 1924  opeldm 2534  enrefg 3294  f1oeng 3298  f1domg 3299  unfilem3 3440  inf5 3472  oncard 3636  cflem 3700  cflecard 3707  ltexpri 3943  recexpr 3954  suppr 3957

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org