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  27316  madebdaylemlrcut  27393  cofcut1  27407  cofcutr  27411  upgr1elem  28372  subumgredg2  28542  subupgr  28544  upgrreslem  28561  umgrreslem  28562  1hevtxdg1  28763  umgr2v2e  28782  pwrssmgc  32170  tocycfv  32268  cycpm3cl2  32295  fldgensdrg  32404  fldgenssv  32405  fldgenssp  32408  nsgmgclem  32522  nsgmgc  32523  nsgqusf1olem2  32525  ssmxidllem  32589  ssmxidl  32590  minplyirredlem  32769  irngnminplynz  32771  zarcls1  32849  zarclsiin  32851  zart0  32859  ldgenpisyslem1  33161  fmla1  34378  aks4d1p5  40945  aks4d1p8  40952  sticksstones2  40963  fnwe2lem2  41793  fnwe2lem3  41794  onintunirab  41976  naddwordnexlem4  42152  supminfrnmpt  44155  supminfxr  44174  supminfxr2  44179  supminfxrrnmpt  44181  smflimsuplem5  45540  rabsubmgmd  46561  lubprlem  47595  intubeu  47609  unilbeu  47610