Theorem elrabd 3654

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {crab 3418

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459

This theorem is used by:  nnawordex  8625  cofon1  8660  ordtypelem7  9489  oemapvali  9656  rankuni2b  9828  harval2  9995  fin23lem11  10312  fin1a2lem11  10405  pinq  10923  negf1o  11655  uzind4  12941  zsupss  12972  flval3  13861  serge0  14105  expge0  14147  expge1  14148  hashbclem  14502  rlimrege0  15649  lcmgcdlem  16681  phicl2  16844  hashdvds  16851  phisum  16867  pcpremul  16920  prmreclem1  16993  prmreclem3  16995  prmreclem5  16997  ramub  17090  ramub1lem1  17103  ramub1lem2  17104  prmgaplem3  17130  prmgaplem4  17131  prmgaplem5  17132  prmgaplem6  17133  mrcflem  17679  mrcval  17683  isacs1i  17730  coaval  18142  gsumress  18761  rabsubmgmd  18783  issubmd  18887  mhmeql  18908  ghmeql  19332  pmtrval  19544  pmtrrn  19550  symgsssg  19560  symgfisg  19561  psgnunilem5  19587  pgpssslw  19707  efgsfo  19832  oddvdssubg  19948  dprdwd  20106  lmhmeql  21205  ssdifidllem  21513  ssdifidl  21514  cofipsgn  21772  frlmssuvc2  21974  gsumbagdiaglem  22110  psrlidm  22140  psrridm  22141  mplmonmul  22216  mhpmulcl  22341  psdmul  22358  coe1fsupp  22403  dmatmulcl  22686  fctop  23190  cctop  23192  ppttop  23193  pptbas  23194  epttop  23195  ordthauslem  23569  cmpsublem  23585  locfincmp  23712  xkoopn  23775  pthaus  23824  txkgen  23838  xkohaus  23839  xkococnlem  23845  nrmr0reg  23935  fbssfi  24023  filssufilg  24097  uffixsn  24111  ufinffr  24115  ufilen  24116  supnfcls  24206  flimfnfcls  24214  alexsubALTlem4  24236  tmdgsum2  24282  symgtgp  24292  ghmcnp  24301  lmle  25489  iundisj  25736  opnmbllem  25789  vitalilem2  25797  aannenlem2  26521  aalioulem2  26525  radcnv0  26608  jensen  27182  ftalem4  27269  ftalem5  27270  efnnfsumcl  27296  efchtdvds  27352  sqff1o  27375  fsumdvdsdiaglem  27376  dvdsppwf1o  27379  dvdsflf1o  27380  muinv  27386  dchrfi  27448  lgsne0  27528  2lgslem1b  27585  cutbdaybnd  28017  madebdaylemlrcut  28121  sltsbday  28139  cofcut1  28142  cofcutr  28146  noseqinds  28515  onsfi  28578  upgr1elem  29491  subumgredg2  29664  subupgr  29666  upgrreslem  29683  umgrreslem  29684  1hevtxdg1  29885  umgr2v2e  29904  pwrssmgc  33343  tocycfv  33452  cycpm3cl2  33479  elrgspnlem1  33585  elrgspnlem2  33586  elrgspnlem3  33587  elrgspnlem4  33588  elrgspnsubrunlem1  33590  fldgensdrg  33658  fldgenssv  33659  fldgenssp  33662  nsgmgclem  33743  nsgmgc  33744  nsgqusf1olem2  33746  ssmxidllem  33779  ssmxidl  33780  1arithufdlem1  33857  1arithufdlem2  33858  1arithufdlem3  33859  1arithufdlem4  33860  0mplrim  33927  selvply1rhmlema  33931  selvply1rhmlemb  33932  selvply1rhmlem1  33933  selvply1rhmlem2  33934  selvply1rhmlem4  33936  selvply1rhm0  33939  extvfvvcl  33948  extvfvcl  33949  mplmulmvr  33952  evlextv  33955  mplvrpmlem  33956  mplvrpmfgalem  33957  mplvrpmga  33958  mplvrpmmhm  33959  mplvrpmrhm  33960  psrmonmul  33963  psrmonprod  33965  esplyfval0  33977  esplylem  33979  esplyfv1  33982  esplyfvaln  33987  esplyind  33988  minplymindeg  34121  minplyirredlem  34123  irngnminplynz  34125  irredminply  34129  zarcls1  34282  zarclsiin  34284  zart0  34292  ldgenpisyslem1  34577  fmla1  35892  aks4d1p5  42880  aks4d1p8  42887  primrootsunit1  42897  primrootscoprmpow  42899  primrootscoprbij  42902  hashscontpow1  42921  sticksstones2  42947  grpods  42994  unitscyglem1  42995  unitscyglem2  42996  unitscyglem4  42998  supinf  43043  fnwe2lem2  43811  fnwe2lem3  43812  onintunirab  43987  naddwordnexlem4  44161  supminfrnmpt  46192  supminfxr  46211  supminfxr2  46216  supminfxrrnmpt  46218  dvnprodlem1  46693  smflimsuplem5  47571  lubprlem  49773  intubeu  49795  unilbeu  49796