Theorem elrabd 3650

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444

This theorem is referenced by:  nnawordex  8575  cofon1  8610  ordtypelem7  9441  oemapvali  9605  rankuni2b  9777  harval2  9921  fin23lem11  10239  fin1a2lem11  10332  pinq  10850  negf1o  11579  uzind4  12831  zsupss  12862  flval3  13747  serge0  13991  expge0  14033  expge1  14034  hashbclem  14387  rlimrege0  15514  lcmgcdlem  16545  phicl2  16707  hashdvds  16714  phisum  16730  pcpremul  16783  prmreclem1  16856  prmreclem3  16858  prmreclem5  16860  ramub  16953  ramub1lem1  16966  ramub1lem2  16967  prmgaplem3  16993  prmgaplem4  16994  prmgaplem5  16995  prmgaplem6  16996  mrcflem  17541  mrcval  17545  isacs1i  17592  coaval  18004  gsumress  18619  rabsubmgmd  18641  issubmd  18743  mhmeql  18763  ghmeql  19180  pmtrval  19392  pmtrrn  19398  symgsssg  19408  symgfisg  19409  psgnunilem5  19435  pgpssslw  19555  efgsfo  19680  oddvdssubg  19796  dprdwd  19954  lmhmeql  21019  cofipsgn  21560  frlmssuvc2  21762  gsumbagdiaglem  21898  psrlidm  21929  psrridm  21930  mplmonmul  22003  mhpmulcl  22104  psdmul  22121  coe1fsupp  22167  dmatmulcl  22456  fctop  22960  cctop  22962  ppttop  22963  pptbas  22964  epttop  22965  ordthauslem  23339  cmpsublem  23355  locfincmp  23482  xkoopn  23545  pthaus  23594  txkgen  23608  xkohaus  23609  xkococnlem  23615  nrmr0reg  23705  fbssfi  23793  filssufilg  23867  uffixsn  23881  ufinffr  23885  ufilen  23886  supnfcls  23976  flimfnfcls  23984  alexsubALTlem4  24006  tmdgsum2  24052  symgtgp  24062  ghmcnp  24071  lmle  25269  iundisj  25517  opnmbllem  25570  vitalilem2  25578  aannenlem2  26305  aalioulem2  26309  radcnv0  26393  jensen  26967  ftalem4  27054  ftalem5  27055  efnnfsumcl  27081  efchtdvds  27137  sqff1o  27160  fsumdvdsdiaglem  27161  dvdsppwf1o  27164  dvdsflf1o  27165  muinv  27171  dchrfi  27234  lgsne0  27314  2lgslem1b  27371  cutbdaybnd  27803  madebdaylemlrcut  27907  sltsbday  27925  cofcut1  27928  cofcutr  27932  noseqinds  28301  onsfi  28364  upgr1elem  29197  subumgredg2  29370  subupgr  29372  upgrreslem  29389  umgrreslem  29390  1hevtxdg1  29592  umgr2v2e  29611  pwrssmgc  33092  tocycfv  33202  cycpm3cl2  33229  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem3  33337  elrgspnlem4  33338  elrgspnsubrunlem1  33340  fldgensdrg  33407  fldgenssv  33408  fldgenssp  33411  nsgmgclem  33503  nsgmgc  33504  nsgqusf1olem2  33506  ssdifidllem  33548  ssdifidl  33549  ssmxidllem  33565  ssmxidl  33566  1arithufdlem1  33636  1arithufdlem2  33637  1arithufdlem3  33638  1arithufdlem4  33639  extvfvvcl  33711  extvfvcl  33712  mplmulmvr  33715  evlextv  33718  mplvrpmlem  33719  mplvrpmfgalem  33720  mplvrpmga  33721  mplvrpmmhm  33722  mplvrpmrhm  33723  psrmonmul  33726  psrmonprod  33728  esplyfval0  33740  esplylem  33742  esplyfv1  33745  esplyfvaln  33750  esplyind  33751  minplymindeg  33885  minplyirredlem  33887  irngnminplynz  33889  irredminply  33893  zarcls1  34046  zarclsiin  34048  zart0  34056  ldgenpisyslem1  34340  fmla1  35600  aks4d1p5  42447  aks4d1p8  42454  primrootsunit1  42464  primrootscoprmpow  42466  primrootscoprbij  42469  hashscontpow1  42488  sticksstones2  42514  grpods  42561  unitscyglem1  42562  unitscyglem2  42563  unitscyglem4  42565  supinf  42609  fnwe2lem2  43405  fnwe2lem3  43406  onintunirab  43581  naddwordnexlem4  43755  supminfrnmpt  45800  supminfxr  45819  supminfxr2  45824  supminfxrrnmpt  45826  dvnprodlem1  46301  smflimsuplem5  47179  lubprlem  49318  intubeu  49340  unilbeu  49341