Theorem elrab3 3332

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 3331	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
3	2	baib 942	1 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175

This theorem is referenced by:  unimax  4409  fnelfp  6346  fnelnfp  6348  fnse  7181  fin23lem30  9047  isf32lem5  9062  negn0  10338  ublbneg  11649  supminf  11651  sadval  15016  smuval  15041  dvdslcm  15149  dvdslcmf  15182  isacs1i  16141  isinito  16473  istermo  16474  subgacs  17452  nsgacs  17453  odngen  17815  lssacs  18788  mretopd  20706  txkgen  21265  xkoco1cn  21270  xkoco2cn  21271  xkoinjcn  21300  ordthmeolem  21414  shft2rab  23083  sca2rab  23087  lhop1lem  23580  ftalem5  24603  vmasum  24741  israg  25392  ebtwntg  25662  nbgranself  25963  eupath2lem3  26506  cvmliftmolem1  30517  nobndlem5  31095  nobndup  31099  nobnddown  31100  neibastop3  31527  fdc  32711  pclvalN  34194  dvhb1dimN  35292  hdmaplkr  36223  diophren  36395  islmodfg  36657  sdrgacs  36790  fsovcnvlem  37327  ntrneiel  37399  radcnvrat  37535  stoweidlem34  38927  eupth2lem3lem3  41398  eupth2lem3lem4  41399  eupth2lem3lem6  41401