Theorem elrabd 3651

Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3649. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
elrabd.1	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))
elrabd.2	⊢ (𝜑 → 𝐴 ∈ 𝐵)
elrabd.3	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
elrabd	⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓})

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

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

Proof of Theorem elrabd

Step	Hyp	Ref	Expression
1		elrabd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		elrabd.3	. 2 ⊢ (𝜑 → 𝜒)
3		elrabd.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))
4	3	elrab 3649	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓} ↔ (𝐴 ∈ 𝐵 ∧ 𝜒))
5	1, 2, 4	sylanbrc 592	1 ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  {crab 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455

This theorem is referenced by:  nnawordex  8601  cofon1  8636  ordtypelem7  9466  oemapvali  9633  rankuni2b  9805  harval2  9949  fin23lem11  10268  fin1a2lem11  10361  pinq  10879  negf1o  11611  uzind4  12901  zsupss  12932  flval3  13819  serge0  14063  expge0  14105  expge1  14106  hashbclem  14459  rlimrege0  15597  lcmgcdlem  16631  phicl2  16794  hashdvds  16801  phisum  16817  pcpremul  16870  prmreclem1  16943  prmreclem3  16945  prmreclem5  16947  ramub  17040  ramub1lem1  17053  ramub1lem2  17054  prmgaplem3  17080  prmgaplem4  17081  prmgaplem5  17082  prmgaplem6  17083  mrcflem  17629  mrcval  17633  isacs1i  17680  coaval  18092  gsumress  18707  rabsubmgmd  18729  issubmd  18831  mhmeql  18851  ghmeql  19270  pmtrval  19482  pmtrrn  19488  symgsssg  19498  symgfisg  19499  psgnunilem5  19525  pgpssslw  19645  efgsfo  19770  oddvdssubg  19886  dprdwd  20044  lmhmeql  21110  cofipsgn  21633  frlmssuvc2  21835  gsumbagdiaglem  21971  psrlidm  22001  psrridm  22002  mplmonmul  22077  mhpmulcl  22202  psdmul  22219  coe1fsupp  22264  dmatmulcl  22548  fctop  23052  cctop  23054  ppttop  23055  pptbas  23056  epttop  23057  ordthauslem  23431  cmpsublem  23447  locfincmp  23574  xkoopn  23637  pthaus  23686  txkgen  23700  xkohaus  23701  xkococnlem  23707  nrmr0reg  23797  fbssfi  23885  filssufilg  23959  uffixsn  23973  ufinffr  23977  ufilen  23978  supnfcls  24068  flimfnfcls  24076  alexsubALTlem4  24098  tmdgsum2  24144  symgtgp  24154  ghmcnp  24163  lmle  25351  iundisj  25598  opnmbllem  25651  vitalilem2  25659  aannenlem2  26381  aalioulem2  26385  radcnv0  26467  jensen  27041  ftalem4  27128  ftalem5  27129  efnnfsumcl  27155  efchtdvds  27211  sqff1o  27234  fsumdvdsdiaglem  27235  dvdsppwf1o  27238  dvdsflf1o  27239  muinv  27245  dchrfi  27307  lgsne0  27387  2lgslem1b  27444  cutbdaybnd  27876  madebdaylemlrcut  27980  sltsbday  27998  cofcut1  28001  cofcutr  28005  noseqinds  28374  onsfi  28437  upgr1elem  29270  subumgredg2  29443  subupgr  29445  upgrreslem  29462  umgrreslem  29463  1hevtxdg1  29664  umgr2v2e  29683  pwrssmgc  33139  tocycfv  33250  cycpm3cl2  33277  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnlem3  33386  elrgspnlem4  33387  elrgspnsubrunlem1  33389  fldgensdrg  33462  fldgenssv  33463  fldgenssp  33466  nsgmgclem  33558  nsgmgc  33559  nsgqusf1olem2  33561  ssdifidllem  33604  ssdifidl  33605  ssmxidllem  33622  ssmxidl  33623  1arithufdlem1  33701  1arithufdlem2  33702  1arithufdlem3  33703  1arithufdlem4  33704  0mplrim  33772  selvply1rhmlema  33776  selvply1rhmlemb  33777  selvply1rhmlem1  33778  selvply1rhmlem2  33779  selvply1rhmlem4  33781  selvply1rhm0  33784  extvfvvcl  33793  extvfvcl  33794  mplmulmvr  33797  evlextv  33800  mplvrpmlem  33801  mplvrpmfgalem  33802  mplvrpmga  33803  mplvrpmmhm  33804  mplvrpmrhm  33805  psrmonmul  33808  psrmonprod  33810  esplyfval0  33822  esplylem  33824  esplyfv1  33827  esplyfvaln  33832  esplyind  33833  minplymindeg  33966  minplyirredlem  33968  irngnminplynz  33970  irredminply  33974  zarcls1  34127  zarclsiin  34129  zart0  34137  ldgenpisyslem1  34421  fmla1  35698  aks4d1p5  42658  aks4d1p8  42665  primrootsunit1  42675  primrootscoprmpow  42677  primrootscoprbij  42680  hashscontpow1  42699  sticksstones2  42725  grpods  42772  unitscyglem1  42773  unitscyglem2  42774  unitscyglem4  42776  supinf  42819  fnwe2lem2  43589  fnwe2lem3  43590  onintunirab  43765  naddwordnexlem4  43939  supminfrnmpt  45980  supminfxr  45999  supminfxr2  46004  supminfxrrnmpt  46006  dvnprodlem1  46481  smflimsuplem5  47359  lubprlem  49544  intubeu  49566  unilbeu  49567