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 583	1 ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {crab 3405

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448

This theorem is referenced by:  nnawordex  8589  cofon1  8623  ordtypelem7  9469  oemapvali  9629  rankuni2b  9798  harval2  9942  fin23lem11  10262  fin1a2lem11  10355  pinq  10872  negf1o  11594  uzind4  12840  zsupss  12871  flval3  13730  serge0  13972  expge0  14014  expge1  14015  hashbclem  14361  rlimrege0  15473  lcmgcdlem  16493  phicl2  16651  hashdvds  16658  phisum  16673  pcpremul  16726  prmreclem1  16799  prmreclem3  16801  prmreclem5  16803  ramub  16896  ramub1lem1  16909  ramub1lem2  16910  prmgaplem3  16936  prmgaplem4  16937  prmgaplem5  16938  prmgaplem6  16939  mrcflem  17500  mrcval  17504  isacs1i  17551  coaval  17968  gsumress  18551  issubmd  18631  mhmeql  18650  ghmeql  19045  pmtrval  19247  pmtrrn  19253  symgsssg  19263  symgfisg  19264  psgnunilem5  19290  pgpssslw  19410  efgsfo  19535  oddvdssubg  19647  dprdwd  19804  lmhmeql  20573  cofipsgn  21034  frlmssuvc2  21238  gsumbagdiaglemOLD  21377  gsumbagdiaglem  21380  psrlidm  21409  psrridm  21410  mplmonmul  21474  mhpmulcl  21576  coe1fsupp  21622  dmatmulcl  21886  fctop  22391  cctop  22393  ppttop  22394  pptbas  22395  epttop  22396  ordthauslem  22771  cmpsublem  22787  locfincmp  22914  xkoopn  22977  pthaus  23026  txkgen  23040  xkohaus  23041  xkococnlem  23047  nrmr0reg  23137  fbssfi  23225  filssufilg  23299  uffixsn  23313  ufinffr  23317  ufilen  23318  supnfcls  23408  flimfnfcls  23416  alexsubALTlem4  23438  tmdgsum2  23484  symgtgp  23494  ghmcnp  23503  lmle  24702  iundisj  24949  opnmbllem  25002  vitalilem2  25010  aannenlem2  25726  aalioulem2  25730  radcnv0  25812  jensen  26375  ftalem4  26462  ftalem5  26463  efnnfsumcl  26489  efchtdvds  26545  sqff1o  26568  fsumdvdsdiaglem  26569  dvdsppwf1o  26572  dvdsflf1o  26573  muinv  26579  dchrfi  26640  lgsne0  26720  2lgslem1b  26777  scutbdaybnd  27197  madebdaylemlrcut  27271  cofcut1  27282  cofcutr  27286  upgr1elem  28126  subumgredg2  28296  subupgr  28298  upgrreslem  28315  umgrreslem  28316  1hevtxdg1  28517  umgr2v2e  28536  pwrssmgc  31930  tocycfv  32028  cycpm3cl2  32055  fldgensdrg  32152  fldgenssv  32153  fldgenssp  32156  nsgmgclem  32263  nsgmgc  32264  nsgqusf1olem2  32266  ssmxidllem  32314  ssmxidl  32315  zarcls1  32539  zarclsiin  32541  zart0  32549  ldgenpisyslem1  32851  fmla1  34068  aks4d1p5  40610  aks4d1p8  40617  sticksstones2  40628  fnwe2lem2  41436  fnwe2lem3  41437  onintunirab  41619  naddwordnexlem4  41795  supminfrnmpt  43800  supminfxr  43819  supminfxr2  43824  supminfxrrnmpt  43826  smflimsuplem5  45185  rabsubmgmd  46205  lubprlem  47115  intubeu  47129  unilbeu  47130