Theorem elrabd 3673

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461

This theorem is referenced by:  nnawordex  8649  cofon1  8684  ordtypelem7  9538  oemapvali  9698  rankuni2b  9867  harval2  10011  fin23lem11  10331  fin1a2lem11  10424  pinq  10941  negf1o  11667  uzind4  12922  zsupss  12953  flval3  13832  serge0  14074  expge0  14116  expge1  14117  hashbclem  14470  rlimrege0  15595  lcmgcdlem  16625  phicl2  16787  hashdvds  16794  phisum  16810  pcpremul  16863  prmreclem1  16936  prmreclem3  16938  prmreclem5  16940  ramub  17033  ramub1lem1  17046  ramub1lem2  17047  prmgaplem3  17073  prmgaplem4  17074  prmgaplem5  17075  prmgaplem6  17076  mrcflem  17618  mrcval  17622  isacs1i  17669  coaval  18081  gsumress  18660  rabsubmgmd  18682  issubmd  18784  mhmeql  18804  ghmeql  19222  pmtrval  19432  pmtrrn  19438  symgsssg  19448  symgfisg  19449  psgnunilem5  19475  pgpssslw  19595  efgsfo  19720  oddvdssubg  19836  dprdwd  19994  lmhmeql  21013  cofipsgn  21553  frlmssuvc2  21755  gsumbagdiaglem  21890  psrlidm  21922  psrridm  21923  mplmonmul  21994  mhpmulcl  22087  psdmul  22104  coe1fsupp  22150  dmatmulcl  22438  fctop  22942  cctop  22944  ppttop  22945  pptbas  22946  epttop  22947  ordthauslem  23321  cmpsublem  23337  locfincmp  23464  xkoopn  23527  pthaus  23576  txkgen  23590  xkohaus  23591  xkococnlem  23597  nrmr0reg  23687  fbssfi  23775  filssufilg  23849  uffixsn  23863  ufinffr  23867  ufilen  23868  supnfcls  23958  flimfnfcls  23966  alexsubALTlem4  23988  tmdgsum2  24034  symgtgp  24044  ghmcnp  24053  lmle  25253  iundisj  25501  opnmbllem  25554  vitalilem2  25562  aannenlem2  26289  aalioulem2  26293  radcnv0  26377  jensen  26951  ftalem4  27038  ftalem5  27039  efnnfsumcl  27065  efchtdvds  27121  sqff1o  27144  fsumdvdsdiaglem  27145  dvdsppwf1o  27148  dvdsflf1o  27149  muinv  27155  dchrfi  27218  lgsne0  27298  2lgslem1b  27355  scutbdaybnd  27779  madebdaylemlrcut  27862  cofcut1  27880  cofcutr  27884  noseqinds  28239  onsfi  28299  upgr1elem  29091  subumgredg2  29264  subupgr  29266  upgrreslem  29283  umgrreslem  29284  1hevtxdg1  29486  umgr2v2e  29505  pwrssmgc  32980  tocycfv  33120  cycpm3cl2  33147  elrgspnlem1  33237  elrgspnlem2  33238  elrgspnlem3  33239  elrgspnlem4  33240  elrgspnsubrunlem1  33242  fldgensdrg  33308  fldgenssv  33309  fldgenssp  33312  nsgmgclem  33426  nsgmgc  33427  nsgqusf1olem2  33429  ssdifidllem  33471  ssdifidl  33472  ssmxidllem  33488  ssmxidl  33489  1arithufdlem1  33559  1arithufdlem2  33560  1arithufdlem3  33561  1arithufdlem4  33562  minplymindeg  33742  minplyirredlem  33744  irngnminplynz  33746  irredminply  33750  zarcls1  33900  zarclsiin  33902  zart0  33910  ldgenpisyslem1  34194  fmla1  35409  aks4d1p5  42093  aks4d1p8  42100  primrootsunit1  42110  primrootscoprmpow  42112  primrootscoprbij  42115  hashscontpow1  42134  sticksstones2  42160  grpods  42207  unitscyglem1  42208  unitscyglem2  42209  unitscyglem4  42211  supinf  42293  fnwe2lem2  43075  fnwe2lem3  43076  onintunirab  43251  naddwordnexlem4  43425  supminfrnmpt  45472  supminfxr  45491  supminfxr2  45496  supminfxrrnmpt  45498  dvnprodlem1  45975  smflimsuplem5  46853  lubprlem  48936  intubeu  48958  unilbeu  48959