Theorem elrabd 3644

Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3642. (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 3642	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓} ↔ (𝐴 ∈ 𝐵 ∧ 𝜒))
5	1, 2, 4	sylanbrc 583	1 ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  {crab 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438

This theorem is referenced by:  nnawordex  8547  cofon1  8582  ordtypelem7  9405  oemapvali  9569  rankuni2b  9741  harval2  9885  fin23lem11  10203  fin1a2lem11  10296  pinq  10813  negf1o  11542  uzind4  12799  zsupss  12830  flval3  13714  serge0  13958  expge0  14000  expge1  14001  hashbclem  14354  rlimrege0  15481  lcmgcdlem  16512  phicl2  16674  hashdvds  16681  phisum  16697  pcpremul  16750  prmreclem1  16823  prmreclem3  16825  prmreclem5  16827  ramub  16920  ramub1lem1  16933  ramub1lem2  16934  prmgaplem3  16960  prmgaplem4  16961  prmgaplem5  16962  prmgaplem6  16963  mrcflem  17507  mrcval  17511  isacs1i  17558  coaval  17970  gsumress  18585  rabsubmgmd  18607  issubmd  18709  mhmeql  18729  ghmeql  19146  pmtrval  19358  pmtrrn  19364  symgsssg  19374  symgfisg  19375  psgnunilem5  19401  pgpssslw  19521  efgsfo  19646  oddvdssubg  19762  dprdwd  19920  lmhmeql  20984  cofipsgn  21525  frlmssuvc2  21727  gsumbagdiaglem  21862  psrlidm  21894  psrridm  21895  mplmonmul  21966  mhpmulcl  22059  psdmul  22076  coe1fsupp  22122  dmatmulcl  22410  fctop  22914  cctop  22916  ppttop  22917  pptbas  22918  epttop  22919  ordthauslem  23293  cmpsublem  23309  locfincmp  23436  xkoopn  23499  pthaus  23548  txkgen  23562  xkohaus  23563  xkococnlem  23569  nrmr0reg  23659  fbssfi  23747  filssufilg  23821  uffixsn  23835  ufinffr  23839  ufilen  23840  supnfcls  23930  flimfnfcls  23938  alexsubALTlem4  23960  tmdgsum2  24006  symgtgp  24016  ghmcnp  24025  lmle  25223  iundisj  25471  opnmbllem  25524  vitalilem2  25532  aannenlem2  26259  aalioulem2  26263  radcnv0  26347  jensen  26921  ftalem4  27008  ftalem5  27009  efnnfsumcl  27035  efchtdvds  27091  sqff1o  27114  fsumdvdsdiaglem  27115  dvdsppwf1o  27118  dvdsflf1o  27119  muinv  27125  dchrfi  27188  lgsne0  27268  2lgslem1b  27325  scutbdaybnd  27751  madebdaylemlrcut  27839  cofcut1  27859  cofcutr  27863  noseqinds  28218  onsfi  28278  upgr1elem  29085  subumgredg2  29258  subupgr  29260  upgrreslem  29277  umgrreslem  29278  1hevtxdg1  29480  umgr2v2e  29499  pwrssmgc  32973  tocycfv  33070  cycpm3cl2  33097  elrgspnlem1  33201  elrgspnlem2  33202  elrgspnlem3  33203  elrgspnlem4  33204  elrgspnsubrunlem1  33206  fldgensdrg  33272  fldgenssv  33273  fldgenssp  33276  nsgmgclem  33368  nsgmgc  33369  nsgqusf1olem2  33371  ssdifidllem  33413  ssdifidl  33414  ssmxidllem  33430  ssmxidl  33431  1arithufdlem1  33501  1arithufdlem2  33502  1arithufdlem3  33503  1arithufdlem4  33504  mplvrpmlem  33565  mplvrpmfgalem  33566  mplvrpmga  33567  mplvrpmmhm  33568  mplvrpmrhm  33569  esplylem  33579  esplyfv1  33582  minplymindeg  33713  minplyirredlem  33715  irngnminplynz  33717  irredminply  33721  zarcls1  33874  zarclsiin  33876  zart0  33884  ldgenpisyslem1  34168  fmla1  35423  aks4d1p5  42113  aks4d1p8  42120  primrootsunit1  42130  primrootscoprmpow  42132  primrootscoprbij  42135  hashscontpow1  42154  sticksstones2  42180  grpods  42227  unitscyglem1  42228  unitscyglem2  42229  unitscyglem4  42231  supinf  42275  fnwe2lem2  43084  fnwe2lem3  43085  onintunirab  43260  naddwordnexlem4  43434  supminfrnmpt  45483  supminfxr  45502  supminfxr2  45507  supminfxrrnmpt  45509  dvnprodlem1  45984  smflimsuplem5  46862  lubprlem  48993  intubeu  49015  unilbeu  49016