Theorem elrab3 3660

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.)

Hypothesis

Ref	Expression
elrab.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elrab3	⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrab3

Step	Hyp	Ref	Expression
1		elrab.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	elrab 3659	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
3	2	baib 535	1 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {crab 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449

This theorem is referenced by:  unimax  4908  fnelfp  7149  fnelnfp  7151  fnse  8112  fin23lem30  10295  isf32lem5  10310  negn0  11607  ublbneg  12892  supminf  12894  sadval  16426  smuval  16451  dvdslcm  16568  dvdslcmf  16601  isprm2lem  16651  isacs1i  17618  isinito  17958  istermo  17959  subgacs  19093  nsgacs  19094  odngen  19507  sdrgacs  20710  lssacs  20873  mretopd  22979  txkgen  23539  xkoco1cn  23544  xkoco2cn  23545  xkoinjcn  23574  ordthmeolem  23688  shft2rab  25409  sca2rab  25413  lhop1lem  25918  ftalem5  26987  vmasum  27127  eqscut2  27718  elmade  27779  israg  28624  ebtwntg  28909  eupth2lem3lem3  30159  eupth2lem3lem4  30160  eupth2lem3lem6  30162  cycpmco2lem1  33083  cycpmco2lem4  33086  cycpmco2  33090  ssdifidllem  33427  1arithufdlem2  33516  tgoldbachgt  34654  cvmliftmolem1  35268  neibastop3  36350  fdc  37739  pclvalN  39884  dvhb1dimN  40980  hdmaplkr  41907  aks4d1p8  42075  sticksstones1  42134  fsuppssind  42581  diophren  42801  islmodfg  43058  fsovcnvlem  44002  ntrneiel  44070  radcnvrat  44303  supminfxr  45460  stoweidlem34  46032