Theorem elrab 1908

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 973	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 973	. 2 |- (y e. B -> A.x y e. B)
3		ax-17 973	. 2 |- (ps -> A.xps)
4		elrab.1	. 2 |- (x = A -> (ph <-> ps))
5	1, 2, 3, 4	elrabf 1907	1 |- (A e. {x e. B | ph} <-> (A e. B /\ ps))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 958   e. wcel 960  {crab 1651

This theorem is referenced by:  elrab3 1909  elrab2 1910  unimax 2536  ssintub 2555  rabxfr 2908  onintss 3017  onnminsb 3022  dfom2 3139  omssnlim 3151  ssnlim 3173  ssimaex 3774  canth 3913  rankr1 4684  rankuni2 4700  rankeq0 4706  scottex 4726  ac6 4765  kmlem1 4775  zorn2lem7 4804  oncardid 4831  cardonle 4832  cardid 4838  iscard2 4865  ondomon 4867  ondomcard 4868  cardmin 4871  alephval2 4913  nnind 5939  infm3 6056  infmsup 6070  infmrcl 6071  peano2uz2 6203  dfuz 6204  uzind 6207  uzind3 6209  uzind3OLD 6211  uzwo4OLD 6212  zmin 6221  flval3t 6241  om2uzuz 6298  om2uzran 6301  uzrdgini 6304  uzrdginip1 6306  elioo1t 6379  elioo2t 6380  elioc1t 6382  elico1t 6383  elicc1t 6384  eluz1t 6421  uzind4 6451  nnwos 6461  elfz1t 6471  seqzvalt 6541  seqz1 6548  sqrval 6672  seq1ublem 6911  clscld 7680  neiint 7716  neips 7724  qdensere 7748  iscn 7755  iscnp 7757  blfval2 7833  blval 7834  elbl 7835  blrn2 7839  blss 7850  iscau 7933  bcthlem4 7999  bcthlem12 8007  bcthlem14 8009  bcthlem32 8027  issubg 8112  sspval 8378  isssp 8379  isblo 8438  ubthlem1 8525  pilog 8763  ocelt 9149  projlem8 9188  shselt 9273  ococint 9292  hsupval2t 9295  chsupsn 9307  shsumval2 9355  elnlfnt 9847  eleigvect 9876  nmcopexlem4 9949  nmcfnexlem4 9978  hmopidmch 10074  shatomistic 10283  hatomistic 10284  elgiso 10393  fgsb 10555  fgsb2 10560  plimfilOLD 10580  iint 10605

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-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  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-rab 1655  df-v 1815

Copyright terms: Public domain