Theorem elrabd 3694

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  {crab 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482

This theorem is referenced by:  nnawordex  8675  cofon1  8710  ordtypelem7  9564  oemapvali  9724  rankuni2b  9893  harval2  10037  fin23lem11  10357  fin1a2lem11  10450  pinq  10967  negf1o  11693  uzind4  12948  zsupss  12979  flval3  13855  serge0  14097  expge0  14139  expge1  14140  hashbclem  14491  rlimrege0  15615  lcmgcdlem  16643  phicl2  16805  hashdvds  16812  phisum  16828  pcpremul  16881  prmreclem1  16954  prmreclem3  16956  prmreclem5  16958  ramub  17051  ramub1lem1  17064  ramub1lem2  17065  prmgaplem3  17091  prmgaplem4  17092  prmgaplem5  17093  prmgaplem6  17094  mrcflem  17649  mrcval  17653  isacs1i  17700  coaval  18113  gsumress  18695  rabsubmgmd  18717  issubmd  18819  mhmeql  18839  ghmeql  19257  pmtrval  19469  pmtrrn  19475  symgsssg  19485  symgfisg  19486  psgnunilem5  19512  pgpssslw  19632  efgsfo  19757  oddvdssubg  19873  dprdwd  20031  lmhmeql  21054  cofipsgn  21611  frlmssuvc2  21815  gsumbagdiaglem  21950  psrlidm  21982  psrridm  21983  mplmonmul  22054  mhpmulcl  22153  psdmul  22170  coe1fsupp  22216  dmatmulcl  22506  fctop  23011  cctop  23013  ppttop  23014  pptbas  23015  epttop  23016  ordthauslem  23391  cmpsublem  23407  locfincmp  23534  xkoopn  23597  pthaus  23646  txkgen  23660  xkohaus  23661  xkococnlem  23667  nrmr0reg  23757  fbssfi  23845  filssufilg  23919  uffixsn  23933  ufinffr  23937  ufilen  23938  supnfcls  24028  flimfnfcls  24036  alexsubALTlem4  24058  tmdgsum2  24104  symgtgp  24114  ghmcnp  24123  lmle  25335  iundisj  25583  opnmbllem  25636  vitalilem2  25644  aannenlem2  26371  aalioulem2  26375  radcnv0  26459  jensen  27032  ftalem4  27119  ftalem5  27120  efnnfsumcl  27146  efchtdvds  27202  sqff1o  27225  fsumdvdsdiaglem  27226  dvdsppwf1o  27229  dvdsflf1o  27230  muinv  27236  dchrfi  27299  lgsne0  27379  2lgslem1b  27436  scutbdaybnd  27860  madebdaylemlrcut  27937  cofcut1  27954  cofcutr  27958  noseqinds  28299  upgr1elem  29129  subumgredg2  29302  subupgr  29304  upgrreslem  29321  umgrreslem  29322  1hevtxdg1  29524  umgr2v2e  29543  pwrssmgc  32990  tocycfv  33129  cycpm3cl2  33156  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrgspnsubrunlem1  33251  fldgensdrg  33316  fldgenssv  33317  fldgenssp  33320  nsgmgclem  33439  nsgmgc  33440  nsgqusf1olem2  33442  ssdifidllem  33484  ssdifidl  33485  ssmxidllem  33501  ssmxidl  33502  1arithufdlem1  33572  1arithufdlem2  33573  1arithufdlem3  33574  1arithufdlem4  33575  minplymindeg  33751  minplyirredlem  33753  irngnminplynz  33755  irredminply  33757  zarcls1  33868  zarclsiin  33870  zart0  33878  ldgenpisyslem1  34164  fmla1  35392  aks4d1p5  42081  aks4d1p8  42088  primrootsunit1  42098  primrootscoprmpow  42100  primrootscoprbij  42103  hashscontpow1  42122  sticksstones2  42148  grpods  42195  unitscyglem1  42196  unitscyglem2  42197  unitscyglem4  42199  supinf  42283  fnwe2lem2  43063  fnwe2lem3  43064  onintunirab  43239  naddwordnexlem4  43414  supminfrnmpt  45456  supminfxr  45475  supminfxr2  45480  supminfxrrnmpt  45482  dvnprodlem1  45961  smflimsuplem5  46839  lubprlem  48859  intubeu  48873  unilbeu  48874