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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {crab 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449

This theorem is referenced by:  nnawordex  8601  cofon1  8636  ordtypelem7  9477  oemapvali  9637  rankuni2b  9806  harval2  9950  fin23lem11  10270  fin1a2lem11  10363  pinq  10880  negf1o  11608  uzind4  12865  zsupss  12896  flval3  13777  serge0  14021  expge0  14063  expge1  14064  hashbclem  14417  rlimrege0  15545  lcmgcdlem  16576  phicl2  16738  hashdvds  16745  phisum  16761  pcpremul  16814  prmreclem1  16887  prmreclem3  16889  prmreclem5  16891  ramub  16984  ramub1lem1  16997  ramub1lem2  16998  prmgaplem3  17024  prmgaplem4  17025  prmgaplem5  17026  prmgaplem6  17027  mrcflem  17567  mrcval  17571  isacs1i  17618  coaval  18030  gsumress  18609  rabsubmgmd  18631  issubmd  18733  mhmeql  18753  ghmeql  19171  pmtrval  19381  pmtrrn  19387  symgsssg  19397  symgfisg  19398  psgnunilem5  19424  pgpssslw  19544  efgsfo  19669  oddvdssubg  19785  dprdwd  19943  lmhmeql  20962  cofipsgn  21502  frlmssuvc2  21704  gsumbagdiaglem  21839  psrlidm  21871  psrridm  21872  mplmonmul  21943  mhpmulcl  22036  psdmul  22053  coe1fsupp  22099  dmatmulcl  22387  fctop  22891  cctop  22893  ppttop  22894  pptbas  22895  epttop  22896  ordthauslem  23270  cmpsublem  23286  locfincmp  23413  xkoopn  23476  pthaus  23525  txkgen  23539  xkohaus  23540  xkococnlem  23546  nrmr0reg  23636  fbssfi  23724  filssufilg  23798  uffixsn  23812  ufinffr  23816  ufilen  23817  supnfcls  23907  flimfnfcls  23915  alexsubALTlem4  23937  tmdgsum2  23983  symgtgp  23993  ghmcnp  24002  lmle  25201  iundisj  25449  opnmbllem  25502  vitalilem2  25510  aannenlem2  26237  aalioulem2  26241  radcnv0  26325  jensen  26899  ftalem4  26986  ftalem5  26987  efnnfsumcl  27013  efchtdvds  27069  sqff1o  27092  fsumdvdsdiaglem  27093  dvdsppwf1o  27096  dvdsflf1o  27097  muinv  27103  dchrfi  27166  lgsne0  27246  2lgslem1b  27303  scutbdaybnd  27727  madebdaylemlrcut  27810  cofcut1  27828  cofcutr  27832  noseqinds  28187  onsfi  28247  upgr1elem  29039  subumgredg2  29212  subupgr  29214  upgrreslem  29231  umgrreslem  29232  1hevtxdg1  29434  umgr2v2e  29453  pwrssmgc  32926  tocycfv  33066  cycpm3cl2  33093  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspnsubrunlem1  33198  fldgensdrg  33264  fldgenssv  33265  fldgenssp  33268  nsgmgclem  33382  nsgmgc  33383  nsgqusf1olem2  33385  ssdifidllem  33427  ssdifidl  33428  ssmxidllem  33444  ssmxidl  33445  1arithufdlem1  33515  1arithufdlem2  33516  1arithufdlem3  33517  1arithufdlem4  33518  minplymindeg  33698  minplyirredlem  33700  irngnminplynz  33702  irredminply  33706  zarcls1  33859  zarclsiin  33861  zart0  33869  ldgenpisyslem1  34153  fmla1  35374  aks4d1p5  42068  aks4d1p8  42075  primrootsunit1  42085  primrootscoprmpow  42087  primrootscoprbij  42090  hashscontpow1  42109  sticksstones2  42135  grpods  42182  unitscyglem1  42183  unitscyglem2  42184  unitscyglem4  42186  supinf  42230  fnwe2lem2  43040  fnwe2lem3  43041  onintunirab  43216  naddwordnexlem4  43390  supminfrnmpt  45441  supminfxr  45460  supminfxr2  45465  supminfxrrnmpt  45467  dvnprodlem1  45944  smflimsuplem5  46822  lubprlem  48950  intubeu  48972  unilbeu  48973