Theorem elrab 1951

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

Hypothesis

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

Assertion

Ref	Expression
elrab	⊢ (A ∈ {x ∈ B∣φ} ↔ (A ∈ B ⋀ ψ))

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

Proof of Theorem elrab

Step	Hyp	Ref	Expression
1		ax-17 1007	. 2 ⊢ (y ∈ A → ∀x y ∈ A)
2		ax-17 1007	. 2 ⊢ (y ∈ B → ∀x y ∈ B)
3		ax-17 1007	. 2 ⊢ (ψ → ∀xψ)
4		elrab.1	. 2 ⊢ (x = A → (φ ↔ ψ))
5	1, 2, 3, 4	elrabf 1950	1 ⊢ (A ∈ {x ∈ B∣φ} ↔ (A ∈ B ⋀ ψ))

Syntax hints:   → wi 3   ↔ wb 144   ⋀ wa 221   = wceq 992   ∈ wcel 994  {crab 1694

This theorem is referenced by:  elrab3 1952  elrab2 1953  unimax 2599  ssintub 2618  onintss 3023  rabxfr 3125  onnminsb 3161  dfom2 3220  omssnlim 3232  ssnlim 3236  ssimaex 3879  canth 4205  rankr1 4820  rankuni2 4836  rankeq0 4842  scottex 4862  ac6 4901  kmlem1 4911  zorn2lem7 4940  oncardid 4967  cardonle 4968  cardid 4975  iscard2 5004  ondomon 5006  ondomcard 5007  cardmin 5010  alephval2 5052  nnind 6082  infm3 6222  infmsup 6236  infmrcl 6237  peano2uz2 6372  dfuzi 6373  uzind 6376  uzind3 6378  uzind3OLD 6380  uzwo4OLD 6381  zmin 6391  flval3 6438  elioo1 6504  elioo2 6505  elioc1 6507  elico1 6508  elicc1 6509  eluz1 6547  uzind4 6577  nnwos 6587  elfz1 6598  om2uzuzi 6660  om2uzrani 6663  uzrdginii 6667  uzrdginip1i 6669  seqzval 6735  seqz1 6742  sqrval 6872  seq1ublem 7114  clscld 7893  neiint 7929  neips 7937  qdensere 7961  iscn 7968  iscnp 7970  blfval2 8046  blval 8047  elbl 8048  blrn2 8052  blss 8063  iscau 8147  bcthlem4 8213  bcthlem12 8221  bcthlem14 8223  bcthlem32 8241  issubg 8358  sspval 8636  isssp 8637  isblo 8697  ishmo 8726  ubthlem1 8787  pilog 9040  ocel 9430  projlem8 9469  shsel 9554  ococin 9573  hsupval2 9576  chsupsn 9588  shsumval2i 9636  elnlfn 10132  eleigvec 10161  nmcopexlem4 10233  nmcfnexlem4 10262  hmopidmchi 10359  shatomistici 10569  hatomistici 10570  elgiso 10683  fgsb 11082  fgsb2 11086  limfillem1 11101  plimfil 11103  iint 11157  cinvlem3 11284  issubcat 11299  issubcata 11300  finminlem 11418  ordtypelem6 11432  ordtypelem7 11433  hartog 11436  onsdom 11437  omsubsuc2 11439  elomsubsd 11446  omsublim 11448  infenomsub 11450  ssntr 11457  compsublem 11487  hscptsscld 11491  alexsublem2 11497  alexsublem4 11499  alexsub 11500  2ndc1stc 11538  isfne3 11543  fneint 11547  fnessref 11564  locfincomp 11575  topmtcl 11586  topmeet 11587  topjoin 11588  opnfbas 11629  elfg 11633  neifg 11644  filssufillem 11655  filssufil 11656  fixufil 11661  isfillim 11676  indexa 11845  nninfnub 11882  sstotbnd 11992  totbndss 11993  totbndbnd 12000  isphtpy 12090

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-rab 1698  df-v 1858

Copyright terms: Public domain