Theorem elrab 1952

Description: Membership in a restricted class abstraction, using 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 1012	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 1012	. 2 |- (y e. B -> A.x y e. B)
3		ax-17 1012	. 2 |- (ps -> A.xps)
4		elrab.1	. 2 |- (x = A -> (ph <-> ps))
5	1, 2, 3, 4	elrabf 1951	1 |- (A e. {x e. B | ph} <-> (A e. B /\ ps))

Syntax hints:   -> wi 3   <-> wb 153   /\ wa 230   = wceq 997   e. wcel 999  {crab 1695

This theorem is referenced by:  elrab3 1953  elrab2 1954  unimax 2586  ssintub 2605  rabxfr 2959  onintss 3068  onnminsb 3073  dfom2 3190  omssnlim 3202  ssnlim 3224  ssimaex 3825  canth 3965  rankr1 4736  rankuni2 4752  rankeq0 4758  scottex 4778  ac6 4817  kmlem1 4827  zorn2lem7 4856  oncardid 4883  cardonle 4884  cardid 4891  iscard2 4919  ondomon 4921  ondomcard 4922  cardmin 4925  alephval2 4967  nnind 5997  infm3 6136  infmsup 6150  infmrcl 6151  peano2uz2 6286  dfuzi 6287  uzind 6290  uzind3 6292  uzind3OLD 6294  uzwo4OLD 6295  zmin 6304  flval3 6351  elioo1 6403  elioo2 6404  elioc1 6406  elico1 6407  elicc1 6408  eluz1 6446  uzind4 6476  nnwos 6486  elfz1 6496  om2uzuzi 6555  om2uzrani 6558  uzrdginii 6562  uzrdginip1i 6564  seqzval 6629  seqz1 6636  sqrval 6761  seq1ublem 7001  clscld 7768  neiint 7804  neips 7812  qdensere 7836  iscn 7843  iscnp 7845  blfval2 7921  blval 7922  elbl 7923  blrn2 7927  blss 7938  iscau 8021  bcthlem4 8087  bcthlem12 8095  bcthlem14 8097  bcthlem32 8115  issubg 8200  sspval 8466  isssp 8467  isblo 8526  ubthlem1 8613  pilog 8851  ocel 9237  projlem8 9276  shsel 9361  ococin 9380  hsupval2 9383  chsupsn 9395  shsumval2i 9443  elnlfn 9935  eleigvec 9964  nmcopexlem4 10037  nmcfnexlem4 10066  hmopidmchi 10162  shatomistici 10372  hatomistici 10373  elgiso 10483  fgsb 10663  fgsb2 10668  plimfilOLD 10688  iint 10716

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-rab 1699  df-v 1859

Copyright terms: Public domain