Theorem elrabd 3686

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477

This theorem is referenced by:  nnawordex  8637  cofon1  8671  ordtypelem7  9519  oemapvali  9679  rankuni2b  9848  harval2  9992  fin23lem11  10312  fin1a2lem11  10405  pinq  10922  negf1o  11644  uzind4  12890  zsupss  12921  flval3  13780  serge0  14022  expge0  14064  expge1  14065  hashbclem  14411  rlimrege0  15523  lcmgcdlem  16543  phicl2  16701  hashdvds  16708  phisum  16723  pcpremul  16776  prmreclem1  16849  prmreclem3  16851  prmreclem5  16853  ramub  16946  ramub1lem1  16959  ramub1lem2  16960  prmgaplem3  16986  prmgaplem4  16987  prmgaplem5  16988  prmgaplem6  16989  mrcflem  17550  mrcval  17554  isacs1i  17601  coaval  18018  gsumress  18601  issubmd  18687  mhmeql  18707  ghmeql  19115  pmtrval  19319  pmtrrn  19325  symgsssg  19335  symgfisg  19336  psgnunilem5  19362  pgpssslw  19482  efgsfo  19607  oddvdssubg  19723  dprdwd  19881  lmhmeql  20666  cofipsgn  21146  frlmssuvc2  21350  gsumbagdiaglemOLD  21491  gsumbagdiaglem  21494  psrlidm  21523  psrridm  21524  mplmonmul  21591  mhpmulcl  21692  coe1fsupp  21738  dmatmulcl  22002  fctop  22507  cctop  22509  ppttop  22510  pptbas  22511  epttop  22512  ordthauslem  22887  cmpsublem  22903  locfincmp  23030  xkoopn  23093  pthaus  23142  txkgen  23156  xkohaus  23157  xkococnlem  23163  nrmr0reg  23253  fbssfi  23341  filssufilg  23415  uffixsn  23429  ufinffr  23433  ufilen  23434  supnfcls  23524  flimfnfcls  23532  alexsubALTlem4  23554  tmdgsum2  23600  symgtgp  23610  ghmcnp  23619  lmle  24818  iundisj  25065  opnmbllem  25118  vitalilem2  25126  aannenlem2  25842  aalioulem2  25846  radcnv0  25928  jensen  26493  ftalem4  26580  ftalem5  26581  efnnfsumcl  26607  efchtdvds  26663  sqff1o  26686  fsumdvdsdiaglem  26687  dvdsppwf1o  26690  dvdsflf1o  26691  muinv  26697  dchrfi  26758  lgsne0  26838  2lgslem1b  26895  scutbdaybnd  27317  madebdaylemlrcut  27394  cofcut1  27409  cofcutr  27413  upgr1elem  28403  subumgredg2  28573  subupgr  28575  upgrreslem  28592  umgrreslem  28593  1hevtxdg1  28794  umgr2v2e  28813  pwrssmgc  32201  tocycfv  32299  cycpm3cl2  32326  fldgensdrg  32435  fldgenssv  32436  fldgenssp  32439  nsgmgclem  32553  nsgmgc  32554  nsgqusf1olem2  32556  ssmxidllem  32620  ssmxidl  32621  minplyirredlem  32800  irngnminplynz  32802  zarcls1  32880  zarclsiin  32882  zart0  32890  ldgenpisyslem1  33192  fmla1  34409  aks4d1p5  40993  aks4d1p8  41000  sticksstones2  41011  fnwe2lem2  41841  fnwe2lem3  41842  onintunirab  42024  naddwordnexlem4  42200  supminfrnmpt  44203  supminfxr  44222  supminfxr2  44227  supminfxrrnmpt  44229  smflimsuplem5  45588  rabsubmgmd  46609  lubprlem  47643  intubeu  47657  unilbeu  47658