Theorem elrabrd 3647

Description: Deduction version of elrab 3644, just like elrabd 3646, 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 3644	. . 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 1569   ∈ wcel 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452

This theorem is used by:  plngcplem  29263  elcgrabasi  29375  cycpmconjslem2  33758  selvply1rhmlemb  34193  selvply1rhm0  34200  extvfvvcl  34209  extvfvcl  34210  mplmulmvr  34213  evlextv  34216  mplvrpmlem  34217  mplvrpmrhm  34221  psrmonprod  34226  esplymhp  34242  esplyfv1  34243  esplyfval3  34246  esplyind  34249  nmuladdel  37003  frlmnzcoordn0  43700