Theorem elrabd 3645

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {crab 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439

This theorem is referenced by:  nnawordex  8561  cofon1  8596  ordtypelem7  9421  oemapvali  9585  rankuni2b  9757  harval2  9901  fin23lem11  10219  fin1a2lem11  10312  pinq  10829  negf1o  11558  uzind4  12810  zsupss  12841  flval3  13726  serge0  13970  expge0  14012  expge1  14013  hashbclem  14366  rlimrege0  15493  lcmgcdlem  16524  phicl2  16686  hashdvds  16693  phisum  16709  pcpremul  16762  prmreclem1  16835  prmreclem3  16837  prmreclem5  16839  ramub  16932  ramub1lem1  16945  ramub1lem2  16946  prmgaplem3  16972  prmgaplem4  16973  prmgaplem5  16974  prmgaplem6  16975  mrcflem  17520  mrcval  17524  isacs1i  17571  coaval  17983  gsumress  18598  rabsubmgmd  18620  issubmd  18722  mhmeql  18742  ghmeql  19159  pmtrval  19371  pmtrrn  19377  symgsssg  19387  symgfisg  19388  psgnunilem5  19414  pgpssslw  19534  efgsfo  19659  oddvdssubg  19775  dprdwd  19933  lmhmeql  20998  cofipsgn  21539  frlmssuvc2  21741  gsumbagdiaglem  21877  psrlidm  21908  psrridm  21909  mplmonmul  21982  mhpmulcl  22083  psdmul  22100  coe1fsupp  22146  dmatmulcl  22435  fctop  22939  cctop  22941  ppttop  22942  pptbas  22943  epttop  22944  ordthauslem  23318  cmpsublem  23334  locfincmp  23461  xkoopn  23524  pthaus  23573  txkgen  23587  xkohaus  23588  xkococnlem  23594  nrmr0reg  23684  fbssfi  23772  filssufilg  23846  uffixsn  23860  ufinffr  23864  ufilen  23865  supnfcls  23955  flimfnfcls  23963  alexsubALTlem4  23985  tmdgsum2  24031  symgtgp  24041  ghmcnp  24050  lmle  25248  iundisj  25496  opnmbllem  25549  vitalilem2  25557  aannenlem2  26284  aalioulem2  26288  radcnv0  26372  jensen  26946  ftalem4  27033  ftalem5  27034  efnnfsumcl  27060  efchtdvds  27116  sqff1o  27139  fsumdvdsdiaglem  27140  dvdsppwf1o  27143  dvdsflf1o  27144  muinv  27150  dchrfi  27213  lgsne0  27293  2lgslem1b  27350  scutbdaybnd  27776  madebdaylemlrcut  27864  cofcut1  27884  cofcutr  27888  noseqinds  28243  onsfi  28303  upgr1elem  29111  subumgredg2  29284  subupgr  29286  upgrreslem  29303  umgrreslem  29304  1hevtxdg1  29506  umgr2v2e  29525  pwrssmgc  33010  tocycfv  33119  cycpm3cl2  33146  elrgspnlem1  33252  elrgspnlem2  33253  elrgspnlem3  33254  elrgspnlem4  33255  elrgspnsubrunlem1  33257  fldgensdrg  33324  fldgenssv  33325  fldgenssp  33328  nsgmgclem  33420  nsgmgc  33421  nsgqusf1olem2  33423  ssdifidllem  33465  ssdifidl  33466  ssmxidllem  33482  ssmxidl  33483  1arithufdlem1  33553  1arithufdlem2  33554  1arithufdlem3  33555  1arithufdlem4  33556  extvfvvcl  33628  extvfvcl  33629  mplmulmvr  33632  evlextv  33635  mplvrpmlem  33636  mplvrpmfgalem  33637  mplvrpmga  33638  mplvrpmmhm  33639  mplvrpmrhm  33640  esplyfval0  33650  esplylem  33652  esplyfv1  33655  esplyind  33659  minplymindeg  33793  minplyirredlem  33795  irngnminplynz  33797  irredminply  33801  zarcls1  33954  zarclsiin  33956  zart0  33964  ldgenpisyslem1  34248  fmla1  35503  aks4d1p5  42246  aks4d1p8  42253  primrootsunit1  42263  primrootscoprmpow  42265  primrootscoprbij  42268  hashscontpow1  42287  sticksstones2  42313  grpods  42360  unitscyglem1  42361  unitscyglem2  42362  unitscyglem4  42364  supinf  42412  fnwe2lem2  43208  fnwe2lem3  43209  onintunirab  43384  naddwordnexlem4  43558  supminfrnmpt  45605  supminfxr  45624  supminfxr2  45629  supminfxrrnmpt  45631  dvnprodlem1  46106  smflimsuplem5  46984  lubprlem  49123  intubeu  49145  unilbeu  49146