Theorem elrabrd 3651

Description: Deduction version of elrab 3648, just like elrabd 3650, but backwards direction. (Contributed by Thierry Arnoux, 15-Jan-2026.)

Hypotheses

Ref	Expression
elrabrd.1	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))
elrabrd.2	⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓})

Assertion

Ref	Expression
elrabrd	⊢ (𝜑 → 𝜒)

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

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem elrabrd

Step	Hyp	Ref	Expression
1		elrabrd.2	. . 3 ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓})
2		elrabrd.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))
3	2	elrab 3648	. . 3 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓} ↔ (𝐴 ∈ 𝐵 ∧ 𝜒))
4	1, 3	sylib 221	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∧ 𝜒))
5	4	simprd 501	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {crab 3414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455

This theorem is used by:  plngcplem  29140  elcgrabasi  29250  cycpmconjslem2  33582  selvply1rhmlemb  34016  selvply1rhm0  34023  extvfvvcl  34032  extvfvcl  34033  mplmulmvr  34036  evlextv  34039  mplvrpmlem  34040  mplvrpmrhm  34044  psrmonprod  34049  esplymhp  34065  esplyfv1  34066  esplyfval3  34069  esplyind  34072  nmuladdel  36779