Theorem elrab3 2841

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331   ∈ wcel 1480  {crab 2420

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rab 2425  df-v 2688

This theorem is referenced by:  unimax  3770  undifexmid  4117  frind  4274  ordtriexmidlem2  4436  ordtriexmid  4437  ordtri2orexmid  4438  onsucelsucexmid  4445  0elsucexmid  4480  ordpwsucexmid  4485  ordtri2or2exmid  4486  acexmidlema  5765  acexmidlemb  5766  isnumi  7038  genpelvl  7320  genpelvu  7321  cauappcvgprlemladdru  7464  cauappcvgprlem1  7467  caucvgprlem1  7487  sup3exmid  8715  supinfneg  9390  infsupneg  9391  supminfex  9392  ublbneg  9405  negm  9407  hashinfuni  10523  infssuzex  11642  gcddvds  11652  dvdslegcd  11653  bezoutlemsup  11697  lcmval  11744  dvdslcm  11750  isprm2lem  11797