Theorem elrab 1422

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

Hypothesis

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

Assertion

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

Distinct variable group(s):   ψ,x   x,A   x,B

Proof of Theorem elrab

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

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   = wceq 1091   ∈ wcel 1092  {crab 1204

This theorem is referenced by:  unisseq 1946  ssintub 1981  onintss 2266  onnminsb 2271  dfom2 2374  omssnlim 2386  ssnlim 2407  canth 2945  oawordeulem 3156  inf3lema 3460  rankr1 3518  rankuni 3533  scottex 3541  ac6 3576  kmlem1 3580  zornlem2 3604  zornlem7 3609  oncardid 3628  cardonle 3629  cardid 3635  iscard2 3660  ondomon 3662  ondomcard 3663  cardmin 3666  elz 4565  peano2uz 4602  uzind2 4604  uzwo 4605  nnwos 4610  uzwo3lem2 4615  zmin 4617  om2uzuz 4653  om2uzran 4655  uzrdgini 4658  sqrval 4729  sqrlem4 4734  ocelt 5162  projlem8 5200  projlem10 5202  projlem13 5205  projlem15 5207  shselt 5280  ococint 5298  hsupval2t 5301  chsupsn 5313  shsumval2 5361  elat 5738  hatomistic 5755

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-rab 1208  df-v 1349

metamath.org