Theorem elrabd 3661

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465

This theorem is referenced by:  nnawordex  8619  cofon1  8654  ordtypelem7  9482  oemapvali  9649  rankuni2b  9821  harval2  9979  fin23lem11  10297  fin1a2lem11  10390  pinq  10908  negf1o  11640  uzind4  12926  zsupss  12957  flval3  13844  serge0  14088  expge0  14130  expge1  14131  hashbclem  14485  rlimrege0  15626  lcmgcdlem  16660  phicl2  16823  hashdvds  16830  phisum  16846  pcpremul  16899  prmreclem1  16972  prmreclem3  16974  prmreclem5  16976  ramub  17069  ramub1lem1  17082  ramub1lem2  17083  prmgaplem3  17109  prmgaplem4  17110  prmgaplem5  17111  prmgaplem6  17112  mrcflem  17658  mrcval  17662  isacs1i  17709  coaval  18121  gsumress  18736  rabsubmgmd  18758  issubmd  18860  mhmeql  18881  ghmeql  19305  pmtrval  19517  pmtrrn  19523  symgsssg  19533  symgfisg  19534  psgnunilem5  19560  pgpssslw  19680  efgsfo  19805  oddvdssubg  19921  dprdwd  20079  lmhmeql  21150  ssdifidllem  21449  ssdifidl  21450  cofipsgn  21708  frlmssuvc2  21910  gsumbagdiaglem  22046  psrlidm  22076  psrridm  22077  mplmonmul  22152  mhpmulcl  22277  psdmul  22294  coe1fsupp  22339  dmatmulcl  22622  fctop  23126  cctop  23128  ppttop  23129  pptbas  23130  epttop  23131  ordthauslem  23505  cmpsublem  23521  locfincmp  23648  xkoopn  23711  pthaus  23760  txkgen  23774  xkohaus  23775  xkococnlem  23781  nrmr0reg  23871  fbssfi  23959  filssufilg  24033  uffixsn  24047  ufinffr  24051  ufilen  24052  supnfcls  24142  flimfnfcls  24150  alexsubALTlem4  24172  tmdgsum2  24218  symgtgp  24228  ghmcnp  24237  lmle  25425  iundisj  25672  opnmbllem  25725  vitalilem2  25733  aannenlem2  26455  aalioulem2  26459  radcnv0  26541  jensen  27115  ftalem4  27202  ftalem5  27203  efnnfsumcl  27229  efchtdvds  27285  sqff1o  27308  fsumdvdsdiaglem  27309  dvdsppwf1o  27312  dvdsflf1o  27313  muinv  27319  dchrfi  27381  lgsne0  27461  2lgslem1b  27518  cutbdaybnd  27950  madebdaylemlrcut  28054  sltsbday  28072  cofcut1  28075  cofcutr  28079  noseqinds  28448  onsfi  28511  upgr1elem  29399  subumgredg2  29572  subupgr  29574  upgrreslem  29591  umgrreslem  29592  1hevtxdg1  29793  umgr2v2e  29812  pwrssmgc  33257  tocycfv  33366  cycpm3cl2  33393  elrgspnlem1  33499  elrgspnlem2  33500  elrgspnlem3  33501  elrgspnlem4  33502  elrgspnsubrunlem1  33504  fldgensdrg  33574  fldgenssv  33575  fldgenssp  33578  nsgmgclem  33660  nsgmgc  33661  nsgqusf1olem2  33663  ssmxidllem  33697  ssmxidl  33698  1arithufdlem1  33775  1arithufdlem2  33776  1arithufdlem3  33777  1arithufdlem4  33778  0mplrim  33845  selvply1rhmlema  33849  selvply1rhmlemb  33850  selvply1rhmlem1  33851  selvply1rhmlem2  33852  selvply1rhmlem4  33854  selvply1rhm0  33857  extvfvvcl  33866  extvfvcl  33867  mplmulmvr  33870  evlextv  33873  mplvrpmlem  33874  mplvrpmfgalem  33875  mplvrpmga  33876  mplvrpmmhm  33877  mplvrpmrhm  33878  psrmonmul  33881  psrmonprod  33883  esplyfval0  33895  esplylem  33897  esplyfv1  33900  esplyfvaln  33905  esplyind  33906  minplymindeg  34039  minplyirredlem  34041  irngnminplynz  34043  irredminply  34047  zarcls1  34200  zarclsiin  34202  zart0  34210  ldgenpisyslem1  34494  fmla1  35774  aks4d1p5  42732  aks4d1p8  42739  primrootsunit1  42749  primrootscoprmpow  42751  primrootscoprbij  42754  hashscontpow1  42773  sticksstones2  42799  grpods  42846  unitscyglem1  42847  unitscyglem2  42848  unitscyglem4  42850  supinf  42893  fnwe2lem2  43663  fnwe2lem3  43664  onintunirab  43839  naddwordnexlem4  44013  supminfrnmpt  46044  supminfxr  46063  supminfxr2  46068  supminfxrrnmpt  46070  dvnprodlem1  46545  smflimsuplem5  47423  lubprlem  49618  intubeu  49640  unilbeu  49641