Theorem elrab 1896

Description: Membership in a restricted class abstraction with implicit substitution.

Hypothesis

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

Assertion

Ref	Expression
elrab	|- (A e. {x e. B | ph} <-> (A e. B /\ ps))

Distinct variable groups:   ps,x   x,A   x,B

Proof of Theorem elrab

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 968	. 2 |- (y e. B -> A.x y e. B)
3		ax-17 968	. 2 |- (ps -> A.xps)
4		elrab.1	. 2 |- (x = A -> (ph <-> ps))
5	1, 2, 3, 4	elrabf 1895	1 |- (A e. {x e. B | ph} <-> (A e. B /\ ps))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  {crab 1640

This theorem is referenced by:  elrab3 1897  elrab2 1898  unimax 2522  ssintub 2541  rabxfr 2892  onintss 3001  onnminsb 3006  dfom2 3123  omssnlim 3135  ssnlim 3157  ssimaex 3753  canth 3892  rankr1 4646  rankuni2 4662  rankeq0 4668  scottex 4688  ac6 4727  kmlem1 4737  zorn2lem7 4766  oncardid 4793  cardonle 4794  cardid 4800  iscard2 4826  ondomon 4828  ondomcard 4829  cardmin 4832  alephval2 4874  nnind 5885  infm3 6001  infmsup 6015  infmrcl 6016  peano2uz2 6149  dfuz 6150  uzind 6153  uzind3 6155  uzind3OLD 6157  uzwo4OLD 6158  zmin 6167  flval3t 6182  om2uzuz 6234  om2uzran 6237  uzrdgini 6240  uzrdginip1 6242  elioo1t 6315  elioo2t 6316  elioc1t 6319  elico1t 6320  elicc1t 6321  eluz1t 6352  uzind4 6382  nnwos 6392  elfz1t 6402  seqzvalt 6472  seqz1 6479  sqrval 6601  seq1ublem 6848  clscld 7625  neiint 7660  neips 7668  qdensere 7691  iscn 7698  iscnp 7700  blfval2 7776  blval 7777  elbl 7778  blrn2 7782  blss 7793  iscau 7874  bcthlem4 7936  bcthlem12 7944  bcthlem14 7946  bcthlem32 7964  issubg 8053  sspval 8316  isssp 8317  isblo 8374  ubthlem1 8460  pilog 8690  ocelt 9070  projlem8 9109  shselt 9193  ococint 9212  hsupval2t 9215  chsupsn 9227  shsumval2 9275  elnlfnt 9768  eleigvect 9797  nmcopexlem4 9869  nmcfnexlem4 9898  hmopidmch 9990  shatomistic 10196  hatomistic 10197  elgiso 10303  fgsb 10444  fgsb2 10449  iint 10478

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-rab 1644  df-v 1803

Copyright terms: Public domain