Theorem elrabd 3710

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490

This theorem is referenced by:  nnawordex  8693  cofon1  8728  ordtypelem7  9593  oemapvali  9753  rankuni2b  9922  harval2  10066  fin23lem11  10386  fin1a2lem11  10479  pinq  10996  negf1o  11720  uzind4  12971  zsupss  13002  flval3  13866  serge0  14107  expge0  14149  expge1  14150  hashbclem  14501  rlimrege0  15625  lcmgcdlem  16653  phicl2  16815  hashdvds  16822  phisum  16837  pcpremul  16890  prmreclem1  16963  prmreclem3  16965  prmreclem5  16967  ramub  17060  ramub1lem1  17073  ramub1lem2  17074  prmgaplem3  17100  prmgaplem4  17101  prmgaplem5  17102  prmgaplem6  17103  mrcflem  17664  mrcval  17668  isacs1i  17715  coaval  18135  gsumress  18720  rabsubmgmd  18742  issubmd  18841  mhmeql  18861  ghmeql  19279  pmtrval  19493  pmtrrn  19499  symgsssg  19509  symgfisg  19510  psgnunilem5  19536  pgpssslw  19656  efgsfo  19781  oddvdssubg  19897  dprdwd  20055  lmhmeql  21077  cofipsgn  21634  frlmssuvc2  21838  gsumbagdiaglem  21973  psrlidm  22005  psrridm  22006  mplmonmul  22077  mhpmulcl  22176  psdmul  22193  coe1fsupp  22237  dmatmulcl  22527  fctop  23032  cctop  23034  ppttop  23035  pptbas  23036  epttop  23037  ordthauslem  23412  cmpsublem  23428  locfincmp  23555  xkoopn  23618  pthaus  23667  txkgen  23681  xkohaus  23682  xkococnlem  23688  nrmr0reg  23778  fbssfi  23866  filssufilg  23940  uffixsn  23954  ufinffr  23958  ufilen  23959  supnfcls  24049  flimfnfcls  24057  alexsubALTlem4  24079  tmdgsum2  24125  symgtgp  24135  ghmcnp  24144  lmle  25354  iundisj  25602  opnmbllem  25655  vitalilem2  25663  aannenlem2  26389  aalioulem2  26393  radcnv0  26477  jensen  27050  ftalem4  27137  ftalem5  27138  efnnfsumcl  27164  efchtdvds  27220  sqff1o  27243  fsumdvdsdiaglem  27244  dvdsppwf1o  27247  dvdsflf1o  27248  muinv  27254  dchrfi  27317  lgsne0  27397  2lgslem1b  27454  scutbdaybnd  27878  madebdaylemlrcut  27955  cofcut1  27972  cofcutr  27976  noseqinds  28317  upgr1elem  29147  subumgredg2  29320  subupgr  29322  upgrreslem  29339  umgrreslem  29340  1hevtxdg1  29542  umgr2v2e  29561  pwrssmgc  32973  tocycfv  33102  cycpm3cl2  33129  fldgensdrg  33281  fldgenssv  33282  fldgenssp  33285  nsgmgclem  33404  nsgmgc  33405  nsgqusf1olem2  33407  ssdifidllem  33449  ssdifidl  33450  ssmxidllem  33466  ssmxidl  33467  1arithufdlem1  33537  1arithufdlem2  33538  1arithufdlem3  33539  1arithufdlem4  33540  minplymindeg  33701  minplyirredlem  33703  irngnminplynz  33705  irredminply  33707  zarcls1  33815  zarclsiin  33817  zart0  33825  ldgenpisyslem1  34127  fmla1  35355  aks4d1p5  42037  aks4d1p8  42044  primrootsunit1  42054  primrootscoprmpow  42056  primrootscoprbij  42059  hashscontpow1  42078  sticksstones2  42104  grpods  42151  unitscyglem1  42152  unitscyglem2  42153  unitscyglem4  42155  supinf  42237  fnwe2lem2  43008  fnwe2lem3  43009  onintunirab  43188  naddwordnexlem4  43363  supminfrnmpt  45360  supminfxr  45379  supminfxr2  45384  supminfxrrnmpt  45386  smflimsuplem5  46745  lubprlem  48642  intubeu  48656  unilbeu  48657