Theorem elrab3 2869

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1335   ∈ wcel 2128  {crab 2439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rab 2444  df-v 2714

This theorem is referenced by:  unimax  3806  undifexmid  4154  frind  4312  ordtriexmidlem2  4478  ordtriexmid  4479  ontriexmidim  4480  ordtri2orexmid  4481  onsucelsucexmid  4488  0elsucexmid  4523  ordpwsucexmid  4528  ordtri2or2exmid  4529  ontri2orexmidim  4530  canth  5775  acexmidlema  5812  acexmidlemb  5813  isnumi  7111  genpelvl  7426  genpelvu  7427  cauappcvgprlemladdru  7570  cauappcvgprlem1  7573  caucvgprlem1  7593  sup3exmid  8822  supinfneg  9500  infsupneg  9501  supminfex  9502  ublbneg  9515  negm  9517  hashinfuni  10644  infssuzex  11828  gcddvds  11838  dvdslegcd  11839  bezoutlemsup  11884  lcmval  11931  dvdslcm  11937  isprm2lem  11984