Theorem elab2g 1900

Description: Membership in a class abstraction, using implicit substitution.

Hypotheses

Ref	Expression
elab2g.1	|- (x = A -> (ph <-> ps))
elab2g.2	|- B = {x | ph}

Assertion

Ref	Expression
elab2g	|- (A e. C -> (A e. B <-> ps))

Distinct variable groups:   ps,x   x,A

Proof of Theorem elab2g

Step	Hyp	Ref	Expression
1		elab2g.1	. . 3 |- (x = A -> (ph <-> ps))
2	1	elabg 1899	. 2 |- (A e. C -> (A e. {x | ph} <-> ps))
3		elab2g.2	. . 3 |- B = {x | ph}
4	3	eleq2i 1538	. 2 |- (A e. B <-> A e. {x | ph})
5	2, 4	syl5bb 532	1 |- (A e. C -> (A e. B <-> ps))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956   e. wcel 958  {cab 1463

This theorem is referenced by:  elab2 1901  eldif 2057  elun 2173  elin 2207  elprg 2423  eluni 2506  eliun 2570  eliin 2571  elong 2956  elimag 3407  tfrlem12 3922  elixp2 4349  elnp 5092  istopg 7596  isbasisg 7611  ismet 7798  isgrp 8041  isps 8645  hcau 9051  sh 9078  closedsub 9093  ch2 9114  elcnopt 9783  ellnopt 9784  elunopt 9799  elhmopt 9800  elcnfnt 9809  ellnfnt 9810  stelt 10141  hstelt 10142  elghomlem2 10383  elsymgrn 10401  iseuctopg 10502  isfil 10558

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-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  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