Theorem elrabd 3658

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

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

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 3403  df-v 3446

This theorem is referenced by:  nnawordex  8578  cofon1  8613  ordtypelem7  9453  oemapvali  9613  rankuni2b  9782  harval2  9926  fin23lem11  10246  fin1a2lem11  10339  pinq  10856  negf1o  11584  uzind4  12841  zsupss  12872  flval3  13753  serge0  13997  expge0  14039  expge1  14040  hashbclem  14393  rlimrege0  15521  lcmgcdlem  16552  phicl2  16714  hashdvds  16721  phisum  16737  pcpremul  16790  prmreclem1  16863  prmreclem3  16865  prmreclem5  16867  ramub  16960  ramub1lem1  16973  ramub1lem2  16974  prmgaplem3  17000  prmgaplem4  17001  prmgaplem5  17002  prmgaplem6  17003  mrcflem  17543  mrcval  17547  isacs1i  17594  coaval  18006  gsumress  18585  rabsubmgmd  18607  issubmd  18709  mhmeql  18729  ghmeql  19147  pmtrval  19357  pmtrrn  19363  symgsssg  19373  symgfisg  19374  psgnunilem5  19400  pgpssslw  19520  efgsfo  19645  oddvdssubg  19761  dprdwd  19919  lmhmeql  20938  cofipsgn  21478  frlmssuvc2  21680  gsumbagdiaglem  21815  psrlidm  21847  psrridm  21848  mplmonmul  21919  mhpmulcl  22012  psdmul  22029  coe1fsupp  22075  dmatmulcl  22363  fctop  22867  cctop  22869  ppttop  22870  pptbas  22871  epttop  22872  ordthauslem  23246  cmpsublem  23262  locfincmp  23389  xkoopn  23452  pthaus  23501  txkgen  23515  xkohaus  23516  xkococnlem  23522  nrmr0reg  23612  fbssfi  23700  filssufilg  23774  uffixsn  23788  ufinffr  23792  ufilen  23793  supnfcls  23883  flimfnfcls  23891  alexsubALTlem4  23913  tmdgsum2  23959  symgtgp  23969  ghmcnp  23978  lmle  25177  iundisj  25425  opnmbllem  25478  vitalilem2  25486  aannenlem2  26213  aalioulem2  26217  radcnv0  26301  jensen  26875  ftalem4  26962  ftalem5  26963  efnnfsumcl  26989  efchtdvds  27045  sqff1o  27068  fsumdvdsdiaglem  27069  dvdsppwf1o  27072  dvdsflf1o  27073  muinv  27079  dchrfi  27142  lgsne0  27222  2lgslem1b  27279  scutbdaybnd  27703  madebdaylemlrcut  27786  cofcut1  27804  cofcutr  27808  noseqinds  28163  onsfi  28223  upgr1elem  29015  subumgredg2  29188  subupgr  29190  upgrreslem  29207  umgrreslem  29208  1hevtxdg1  29410  umgr2v2e  29429  pwrssmgc  32899  tocycfv  33039  cycpm3cl2  33066  elrgspnlem1  33166  elrgspnlem2  33167  elrgspnlem3  33168  elrgspnlem4  33169  elrgspnsubrunlem1  33171  fldgensdrg  33237  fldgenssv  33238  fldgenssp  33241  nsgmgclem  33355  nsgmgc  33356  nsgqusf1olem2  33358  ssdifidllem  33400  ssdifidl  33401  ssmxidllem  33417  ssmxidl  33418  1arithufdlem1  33488  1arithufdlem2  33489  1arithufdlem3  33490  1arithufdlem4  33491  minplymindeg  33671  minplyirredlem  33673  irngnminplynz  33675  irredminply  33679  zarcls1  33832  zarclsiin  33834  zart0  33842  ldgenpisyslem1  34126  fmla1  35347  aks4d1p5  42041  aks4d1p8  42048  primrootsunit1  42058  primrootscoprmpow  42060  primrootscoprbij  42063  hashscontpow1  42082  sticksstones2  42108  grpods  42155  unitscyglem1  42156  unitscyglem2  42157  unitscyglem4  42159  supinf  42203  fnwe2lem2  43013  fnwe2lem3  43014  onintunirab  43189  naddwordnexlem4  43363  supminfrnmpt  45414  supminfxr  45433  supminfxr2  45438  supminfxrrnmpt  45440  dvnprodlem1  45917  smflimsuplem5  46795  lubprlem  48923  intubeu  48945  unilbeu  48946